[boost] Re: Invariants Library

From: Thorsten Ottosen (nesotto_at_[hidden])
Date: 2004-01-03 01:38:04

"Dan W." <danw_at_[hidden]> wrote in message
news:bt5l69$j7e$1_at_sea.gmane.org...
> Thorsten Ottosen wrote:

[snip]

> >>Maybe we're talking about different parts of DBC... Okay, variant and
> >>invariants are not meant to be 'public DBC', and should NOT be in the
> >>header file.
> > Not the invariant? I would have said that a part of the invariant that
> > describes
> > certain relationsships between the public value returning functions
would be
> > usefull documentation.
>
> Yeah, first I said that it 'should' be in the header, then I went to say
> that it 'shouldn't'. The thing is, the invariant of a class is
> absolutely nobody-else's business. Sure it documents the class, to the
> implementer;  but a client of the class needs to know nothing about its
> invariants. Invariants ARE documentation;  I totally agree;  but it's
> just not *public* documentation; --rather meant to be an X-file, and be
> kept in the CPP cabinet. On the other hand, the class variables are
> declared in the header file, and the invariants are closely related to
> them... Maybe that's why I like the pimpl idiom so much...

Consider an STL container like vector and its "public" invariant:

begin() <= end();
rbegin() <= rend();
begin() == end() implies empty();
empty() implies size() == 0;
size() >= 0;
capacity() >= size();

I don't think that is "private" business. For sake of debugging, it makes
perfect sense
to have assertions about the private members.

> Postconditions are the product your function sells, and preconditions
> are the price-tag.  It would make no sense to hide them in the cpp file.

I'm aware of what you're trying to say, but we have to remember Eiffel has a
different way of
compiling and linking.

> > the Eiffel headers is already an extract of the source files? No matter
what
> > scheme, you would still
> > have to read the updated documentation (whether a header or something
else).
>
> Precisely, you don't want to read an html doc where you could read a
> much more eloquent hpp doc, which has the built-in guarantee of being in
> synch with the latest code.. ;-)

What if the html consisted of merely the code with assertions, just like an
Eiffel short-form of the class?
The relaese of a new version of a library is usually a bigger step and
recompiling docs, should be rather trivially
automated.

> That's one of the vivid memories I
> have of working with Eiffel: you read through a class header, and every
> line of DBC code is worth 100 lines of dubious plain language
> documentation; and you *know* it's current; and, if it works, accurate.

If you extract the docs by a tool as the last thing you do, you have the
same guarantee.

>    static void insert_char( char* s, int len, int pos, char const & c );
>
> Fairly well written, wouldn't you say? Yet, I'm not sure what happens if
> pos is greater than len. I don't know if MAXLEN is taken care of by the
> caller or not.  I don't know what happens if I give it a null pointer
> for a string. Chances are it throws, or crashes, or maybe it allocates
> the string itself, if it's not there. Who knows? There goes another half
> hour of my precius time looking for where is it documented.. But...
>
>    static void insert_char( char* s, int len, int pos, char const & c )
>    {
>    preconditions:
>       s && strlen(s)==len && pos>=0 && pos<=len && (int)c<128;
>    postconditions:
>       s && len && strlen(s)==len+1 && s[pos]==c;
>    }

sure, that is beside the discussion. The important thing is that you have
access to
such (up-ti-date) documentation, not whether it is an header file or not.

br

Thorsten