Re: [boost] [contract] Contract Programming Library

Subject: Re: [boost] [contract] Contract Programming Library
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-02-18 23:32:02

Hello Andrzej,

Most of your questions are answered by the documentation updates I am
making now. Please see my "preview" answers below.

Note that some of the points you make are "policy" decisions. I listed
what the library currently does, but a different "policy" could be
implemented easily within the library.

On Tue, Feb 16, 2010 at 4:34 AM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
>  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."

No, postconditions are NOT checked if the body throws. However, class
invariants are checked also when the body throws (requirement from
[Crowl2006], see library documentation bibliography).

> (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?).

Object, all function arguments, and result value are passed as
constant references. This is true even if the contracted function is
not a constant member, it has non const& arguments, and non const&
result (the const& is added using Boost.TypeTraits).

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

Assertions appear in constant member function so the can access static
data, etc as usual.
I need to study the rest of your comment above C++(0x lambdas) more...

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

If code checking the contract (invariants, preconditions,
postconditions) throws any exception the contract is considered failed
and the relative failure handler function is invoked (default
std::terminate() but can be redefined by the user). This is because if
it is not possible to check that a contract condition is true, due to
an exception, then the only "safe" thing to do is to assume that the
asserted condition failed.

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

Yes, any public/protected/private member can be accessed by the contracts.

Preconditions should only access public members (otherwise the callers
cannot fully check them) and Eiffel enforces this at compile-time.
However, my library does not enforce this constraint and leaves it up
to programmers to write good preconditions that do not use protected
or private members. (Due to C++ friendship it is somewhat difficult to
fully embrace the argument that preconditions should not access
private members in C++ because even if they do callers that are
friends of the class can still check them...)

Class invariants and postconditions can access non-public members
(also in Eiffel) as their contracts are allowed to the check the
correctness of the implementation (for example invariants assert a
private member pointer is always not null).

In general, I find assertions that use public members to be much more
useful because they are the ones documenting the specifications (not
the implementation).

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

Yes (just implemented and documented).

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

Yes (just implemented and documented). The library supports block
invariants (which can also be used to assert loop invariants) as
specified in [Crowl2006]. Also Eiffel-like loop variants are
supported.

void f(std::vector v, const size_t& n) {
    size_t i = 0;
    CONTRACT_ASSERT_BLOCK_INVARIANT( i == 0 );
    for (CONTRACT_INIT_LOOP_VARIANT; i < v.size(); ++i) {

    }

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

The library follows Eiffel semantics for constructor which is {Default
AND Pre}Body{Post AND Inv} where Default is default initialization of
members (similar to C++ member initialization list). That said, it
would be difficult to implement a different semantics (like the one
you suggest) in C++ because of the lack of delegating constructors.

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

The documentation shows the macros (in Tutorial), the expanded code
(in Without the Macros), and it refers to [Crowl2006] for how language
support would look like. But I will look into your suggestion (I will
study Boost.Interface).