[boost] Re: Invariants Library

From: Dan W. (danw_at_[hidden])
Date: 2004-01-03 02:24:44

Thorsten Ottosen wrote:
> 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.

In this case you're sort of right. But (A) there's something special 
about this class: Notice how you managed to express its invariant using 
nothing but public functions. This class is exposing its guts to the 
world and making them everybody's business. (B) That may or may not be 
the real invariant. In most implementations it is not. You're not 
checking, for example, how much memory is currently allocated. Perhaps 
it recently was as big as 1K bytes, and now it only needs 100 bytes, and 
it should have de-allocated 512 bytes half hour ago and forgot. The 
invariant is supposed to check *everything* that must hold true, NOT 
just what matters to the clients. Thus, what you show is a subset of the 
invariant that is indeed of public concern, and should appear in the 
postconditions of all public functions.

>>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.

If it did it wouldn't matter. The fact is, the contracts must be in the 
open, or else they aren't contracts. In C++, "In the open" == .hpp

> 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.

I'm not opposed to producing documentation from source. All I'm saying 
is that preconditions and postconditions of public functions belong in 
the header file.

>>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.

Sure, I agree. But what's your point?

>>   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.

No. The point is that the header file is what a class advertises about 
itself, and the cpp file is what a class does not advertise.  Its 
products, services and price-list are things it advertises, therefore 
they go in the header file.
The fact that contracts go a long way to document a class, and that 
their concurrency is guaranteed, and the necessity or not for the 
contracts to be in the header file for the sake of compilation and/or 
linkage, are all secondary concerns.