[boost] Re: Invariants Library

From: Thorsten Ottosen (nesotto_at_[hidden])
Date: 2004-01-02 07:33:20

"Dan W." <danw_at_[hidden]> wrote in message
news:bt3k5r$mia$1_at_sea.gmane.org...
[snip]
> Eiffel, AFAIK, is *the* DBC language, and I would hope a C++ effort in
> the DBC direction would take notice of its elegance, features and
> semantics. DBC, in Eiffel, is only compiled-in in debug mode, and it
> serves two purposes: To debug, and to document.

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

> DBC:
> Eiffel has, AFAIR, 4 DBC-related keywords: "invariants", "variant",
> "requires" and "ensures".  There's another keyword in E. that is used a
> lot in DBC code: "implies", as in "bool_expr1 implies bool_expr2;", the
> equivalent of "assert(!bool_expr1 || bool_expr2);".

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

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

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

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

> 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
code would have to be placed/maintained
in headers.

> 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() );

br

Thorsten