Re: [boost] [contract] Contract Programming Library

Subject: Re: [boost] [contract] Contract Programming Library
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2010-02-16 04:34:36

> I am thinking to submit a library for Contract Programming (a.k.a.
> Design By Contract (TM) ) for C++.

> I have drafted some of the library documentation in Boost-like format:
> http://dbcpp.sourceforge.net/boost/libs/contract/doc/html/

> Comments?

 Hi,
 I have a couple of questions/suggestions regarding the documentation
of the library.

 (1)
 Does it execute postconditions when the function body ends with a
thrown exception? Obviously it shouldn't. I can see one lie saying

   It is possible to describe the function postconditions.
   These are logical conditions that programmers expect
   to be true when the function has ended **normally**.

 So I guess it doesn't, but I believe this fact deserves some more
room in the documentation, like "public member function is not
required to satisfy the postcondition if it ends with exception."

(2)
Obviously, the expressions in assertions shouldn't change the
behaviour of the program when executed. This requirement is stronger
than having no side effects. You protect the object itself by allowing
only const member functions. Are the function arguments (those passed
by mutable reference also protected?).
Is it allowed/recommended to refer to global or static data in the
assertions? If you are using clever macros, perhaps there is a way to
block the references to these. In C++0x lambdas you can specify a list
of objects you want to refer to:
  [this, &max_value, &count, &cache]( int fact1, int fact2 ) {...}
perhaps there is a way to do it with current C++ macros.

(3)
In a similar manner, what happens if one of postcondition's assertions
throws an exception? I have troubles answering this question myself (I
do not know what should ideally happen), but whatever your answer is,
I believe it should be clearly documented. (Note that this is not only
the issue of DbC; simple C-assertions also leave this question
unanswered).

(4)
Do the assertions have access to objet's private/protected interfaces?
(I believe they shouldn't).

(5)
Does the library allow defining preand postconditions for "free"
functions or static member functions? The examples are so focused on
objects/classes that I cannot tell the answer.

(6)
Similarly, does the library allow defining block invariants?

(7)
The documentation lists the following sequence for executing a constructor:

   1. Initialize member variables via the constructor member
initialization list (if such a list is specified).
   2. Check preconditions (but not invariants).
   3. Execute constructor body.
   4. Check invariants.
   5. Check postconditions.

I believe, one of the reasons for validating arguments of a constuctor
is to not allow the incorrect values to initialize objest's
sub-objects (members). I believe the sequence of the first two items
should be inverse. Am I wrong?

(8)
Since library usses macros that make the syntax a bit difficult to
read/parse, perhaps it would be useful to augment every example with
another one that would say how the same thing would be acomplished
with fictitious "DbC C++" syntax if we had one. This was done for
Boost Interface library (under construction,
http://www.cdiggins.com/bil.html) and I think it helps a lot.

Regards,
&rzej