[boost] Re: Invariants Library

From: Dan W. (danw_at_[hidden])
Date: 2004-01-02 08:31:58

Thorsten Ottosen wrote:

> I recall that one could choose not to remove preconditions
> from release builds.

In public interfaces no, as the preconditions are in the extracted 
header, but the preconditions in private functions, and all non-public, 
implementation classes in the object code, preconditions are gone.
Wouldn't make sense to keep them without source code to debug.

> and the keyword 'old' used in post-conditions.

Yes, I mentioned it later.

>>invariants:
>>As you might guess, this is like a function containing statements about
>>state coherence of class variables. It is typically defined next to the
>>class variables, above or below them. The compiler, in debug mode, puts
>>a call to this function at the entry and exit points of every *public*
>>function.
> As far as I can tell, then one call either at exit or entry should be
> sufficient.

Yes, you're right. I vote for at exit, the reason being, you want to 
catch the bug immediately, not the next time you enter the class.

>>I cannot remember what the inheritance policy was, at this
>>moment;
> Invariants must be ANDed. A derived class has a stronger or equally strong
> invariant.

Right; in fact, the invariants of a parent class are implicitly embedded 
  with it when inherited.

>>variant:
>>An integer expression used within a loop that must evaluate to a lower
>>value at each iteration, but must never become negative. Helps diagnose
>>loops that might lead to a lock-up.
> what about ascending values?

for( int i = 0; i++ < 1000; )
{
     variant( 1111 - i );
     factorize( i ); //or whatever.
}

>>1) DBC statements should be header-file only, if there's any way to
>>ensure this, so that they are public, available to users of a library,
>>and may so constitute 'documentation'.
> While this might be good for quick and dirty implementation, it would
> totally ruin the
> overview of a class. It will also create more re-compilation because the DBC

"..ruin the overview of a class"?! The class *IS* its contracts!

> code would have to be placed/maintained
> in headers.

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.
Maybe I should have clarified that; sorry, my fault.  But preconditions 
and postconditions in public functions are what defines and documents 
what those public functions demand and promise, for all to see.  If they 
were non-header, it would mean that the contract could be secretly 
altered, without the consent of the class' clients.

>>5) I have code I came up with to implement "implies".  It is coded as a
>>macro that produces ,_impl_dummy_(), and two template overloads of the
>>comma operator:
>>template <expr X> _impl_wrapper_& operator,(X const &, _impl_dummy_&);
>>template <expr X> bool operator,(_impl_wrapper_&, X const &);
>>Or something like that, can't remember. Worked though.
>>I can dig it up if there's interest.
> 
> A macro would do it:
> 
> #define implies  != true ? true :

> and then you can say assert( foo() implies bar() );

Clever, but != has higher precedence than ||, &&, etc;  so you couldn't 
say assert( !foo() && !bar() implies !( foo() || bar() ) );

The 'implies' keyword has ultra-low precedence in Eiffel, and the comma 
operator I think fits it like a glove.

Besides, my little idiom already includes the assert, so you just say,

     !foo() && !bar()  implies  !( foo() || bar() );

Cheers!