[boost] Re: Invariants Library

From: Dan W. (danw_at_[hidden])
Date: 2004-01-02 06:20:25

Reece Dunn wrote:

> cool! But these seem to work via assert which will terminate the program 
> upon invariant failure.
> With C++ having exception support, surely the exception mechanism is a 
> better way to deal with invariants that do not hold? This allows the 
> client code to react to the failure and report something readible to the 
> user, like:
>   invariant failure: cannot access a null pointer, in ...
> instead of something like:
>   abnormal program termination

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.
Although I see your point, I'd prefer not to mix assertions and 
exceptions in a DBC implementation. It would complicate things to no 
end, IMHO.
You can use exceptions, of course, but you code them separately.  The 
behaviour of the Eiffel debugger is not to terminate, rather to stop 
execution upon a DBC violation. A C++ implementation could place coded 
breaks, I suppose.

> Also, you need a compiler that supports the DBC extensions. The current 
> thinking behind the new C++ standard is to adopt a minimal set of 
> language extensions and a large number of library extensions (c.f. 
> Bjarne Stroustrup, et. al.). Having a library-based invariant mechanism 
> (integrating into the exception handling mechanism) allows support for 
> older compilers (GCC 2.95.x; VC6; etc) that do not implement C++0x 
> features.

All very true, but I do hope that DBC gets language support, because if 
it stays implemented just as a library, using it will be "too optional" 
if I may so qualify it... ;-)

>> Design By Contract is such a wonderful concept, BTW, I used to program 
>> in Eiffel, and there's nothing I miss more than its built-in DBC.
> I agree, DBC is a powerful concept. What I am trying to do is open up 
> the discussion on how it should be implemented in C++.

I'm glad to oblige!  May I, under such special circumstances, cross the 
line and talk about another language?  I'd like to give those interested 
in this subject a little tour of Eiffel, and how DBC works in Eiffel, 
but most importantly, *why is it actually USED* by Eiffel programmers, 
so that perhaps we may consider this angle when discussing it.

Begin Eiffel:

For those totally un-familiar with E., it is a compiled, procedural 
language, with most compiler implementations compiling to C.  It is OO, 
supports multiple inheritance in a big way (meaning that if you looked 
at some typical sample E. source code you'd see multiple inheritance 
used and abused everywhere). Functions are virtual by default.  The 
syntax is something between Ada, Pascal, and C. (Someone will shoot me 
now.) It enforces command/query separation: A non-static function is 
either a query (returns non-void, and is const), or a command (is 
non-const, but returns void); --and no 'special case', no way to get 
around it.
It is also garbage-collected (something I personally hated about it), 
and initially had no function overloading at all, though, by arguing 
with Bertrand Meyers at an Eiffel forum, I managed to convince him to 
allow overloading of constructors for the (then) upcoming 
specification... :-]
There are no 'header' files as such;  rather, you declare AND define at 
once into a "classname.e" file for each class.  The compiler extracts 
declaration information on a first pass, and compiles on a second pass. 
  For classes in a library whose interface one wishes to publish, there 
is a separate tool that automatically strips all implementation code out 
of a -.e file, producing a public header file from it.

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);".
Typically, when you work with E., you *begin* with DBC code, as this 
allows you to get early feedback from the compiler in terms of contract 
correctness.  (There are many subtleties to DBC, and achieving such 
correctness is not as trivial as it may sound.)  Psychologically, this 
is a thrilling phase in coding: For each class and each function you're 
feeling identified with the piece of code and thinking like a lawyer: 
"What could the caller possibly throw at me that I haven't thought of?" 
  But it is also like an elections campaign thing: "What else can I 
promise in my postconditions, so that a user will really approve and 
admire what this function can do, or how thoughtful it is?".
When the tool I mentioned earlier is used to extract a 'header' file 
from a -.e file, all requires and ensures (pre-/post-conditions) of 
public functions stay in the header by default (otherwise, an imported, 
object library could not be debugged with user code using DBC). Thus, E. 
code rarely needs comments, since most of what the user needs to know 
about a class is expressed through the DBC code. Eiffel programmers 
would frown hard at seeing a comment that should have been expressed as 
a DBC condition, instead.

requires:
Every function begins, typically, with a requires section, establishing 
range limits for the arguments, making sure there aren't null 
references, and whatever else one may think of requiring.
One subtle aspect of preconditions is that they may NOT access private 
functions in the class. The rationale is that you cannot expect the 
caller to ensure conditions that IT has no way to know, test or verify. 
Else, it would be as if I were to tell you, "You can phone me any time, 
EXCEPT when my cat is sleeping next to the phone...".
Note: Private variables in Eiffel have read-only, public visibility.
I don't remember what the policy was with private variables; I think 
that they couldn't be accessed either, the rationale being that the 
caller can see them, but cannot change them.
Another subtle aspect of preconditions is that they might as well be as 
tight as possible, for they can only be relaxed through inheritance. 
Ie.: if function f() in class A requires X, function f() in derived 
class B cannot require X && Y, for that would violate polymorphism. In 
fact, requires' in B::f() are OR-ed by the compiler with A::f()'s.

ensures:
Every function typically ends with a posconditions section, --the 
"advertising" section. Technically, you can access private members, 
though this doesn't always make sense. Another E. keyword typically used 
with ensures (as well as variant and invariants) is "old", used as a 
qualifier to a variable, function return, or expression;  which causes 
the compiler to compute and save its value on function entry, and helps 
express promised relative changes.
Conversely to requires, ensures are tightened by inheritance. A function 
in a derived class cannot promise less than the same function in the 
parent class, or this would violate polymorphism. Ensures in a derived 
class are ANDed by the compiler with ensures in the parent class 
function, and so one wants to be really careful about promising too 
much, --or too short-sightedly.

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. I cannot remember what the inheritance policy was, at this 
moment; but I would think that derived post conditions are ANDed. They 
are nobody else's business, polymorph-wise, anyhow. Invariants are also 
asserted at the exit points of constructors, and the entry point of 
destructors.

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.

After designing a package of classes using DBC and debugging it as 
necessary for the first phase of compilation to pass, one might decide 
to flesh out the code with actual implementation.  You wouldn't believe 
how easy this is, having DBC code right there:  Trivial as this may 
sound, writing the implementation is made a breeze by being able to copy 
and paste variable/function names and whole expressions, from the 
require and ensure blocks, above and below.
Debugging is, again, enormously accelerated by DBC violation stops:  If 
the requires stops the code, go back to the caller and fix it. If the 
ensures stops the code, fix the function itself.  If invariants stop the 
code, you forgot something.. ;-) If variant stops the code, God bless 
DBC, or the debugger would have crashed!

End Eiffel;

A DBC implementation for C++, IMO, should aim to offer similar 
advantages as Eiffel's implementation:  Not just debugging but 
documentation advantages as well.  It should be as easy to use as it 
takes for it to BE used;  and become a "way of life".

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

2) A good way to implement invariants, IMHO, would be to somehow make 
the statements part of a struct... uh, easier with code:

template< class T >
struct invariants
{
     invariants(T const * t)
#ifdef _DEBUG
     : _(*t)
     {
        _invariants_()
     }
     ~invariants()
     {
        _invariants_()
     }
  private:
     T const & _;
     void _invariants_(T const *)
     {
        assert(0);
     }
     invariants() //no default ctor
#endif
     {}
};
........
class my_class
{
     int a, b;
     my_class() : a(1), b(1) {}
     template<>
     friend invariants< my_class >
     {
        void _invariants_()
        {
            assert( _.a + _.b == 2 );
        }
     };
     typedef invariants< my_class > _chki;
  public:
     void f()
     {
        _chki _(this);
        ++a;
     } //boom!
};

To add invariant checking at the ends of constructors and the beginnings 
of destructors, we'd have to ensure that the invariants struct is also 
instantiated as a class member, and always be the last member.

3) Preconditions and postconditions could be implemented as functors, as 
we cannot define functions inside functions, and don't need access to 
private or protected members anyhow. I've no idea, at this moment, how 
the OR-ing of preconditions and AND-ing of postconditions in the case of 
inheritance could be implemented without language support.

4) Would be nice to have "variant" also.

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.

Cheers!