[boost] [contract] diff n1962

8 Apr 2010

      Hello all,

Below is a summary of the differences between Boost.Contract and the
Contract Programming  C++ standard proposal n1962. I know some of the
authors of n1962, and also of its previous revisions, are on this
mailing list -- I hope that they can provide comments at least.

[n1962] Crowl and T. Ottosen, Proposal to add Contract Programming to
C++ (revision 4), The C++ Standards Committee, 2006. All previous
revisions of this proposal are also relevant (and related authors
comments encouraged).

Boost.Contract design was vastly based on n1962. However, in few
places I deliberately made the different design decisions listed
below. Based on your feedback, I would be happy to revisit my design
decisions to align even more Boost.Contract with n1962.

1) SUBCONTRACTING
n1962 allows only the base class to specify preconditions. Instead,
Boost.Contract allows also derived classes to specify preconditions.

Boost.Contract fully supports subcontracting as defined by
substitution principles, implemented by Eiffel, and specified by
prevision revisions of n1962 (n1613). However, Boost.Contract could be
modified to comply with n1962.

Why does n1962 allow preconditions only for the base classes?

n1962 section 4.2.1: <<If the function F is virtual, we require that
1. only the base virtual function of F can have a precondition.
Section 3.5 of n1613 explains how little redefinition of preconditions
is used. Even though subcontracting is theoretically sound, it ends up
being fairly useless in practice [3].
[3] A weaker precondition can be taken advantage of if we know the
particular type of the object. If weaker preconditions should be
allowed, then there exists two alternatives: to allow reuse of an
existing contract or to require a complete redefinition. The former
favours expressiveness, the latter favours overview.>>.

2) STATIC CLASS INVARIANTS
n1962 does not support static class invariants. Instead,
Boost.Contract supports static class invariants.

Non-static class invariants are not checked at constructor entry, at
destructor exit, and at entry/exit of static member functions (because
there is no object in these cases). Static class invariants instead
are always checked at entry/exit of constructors, destructor, and
(static or non-static) member functions.

I added static class invariants for completeness. Boost.Contract could
drop static class invariants to comply with n1962 (but I find them
useful).

    struct z {
        static int counter;
        int number;

        CONTRACT_CLASS( (z)
        (static) (invariant) ({ // Static class invariants (no object here).
            CONTRACT_ASSERT( counter >= 0 );
        })
        (invariant) ({ // Non-static class invariants (`this` present).
            CONTRACT_ASSERT( number <= counter );
        }) )

        ...
    };

Why does n1962 not support static class invariants?

3) ARBITRARY CODE IN CONTRACTS
n1962 allows only a list of assertions, eventually guarded by
if-statements, in invariants, preconditions, and postconditions.
Instead, Boost.Contract allows for any C++ code in the contract.

Boost.Contract documentation recommends to keep the contract code
simple, limited to a list of assertions eventually guarded by
if-statements (otherwise, it is more likely you have bugs in the
contracts than in the actual code). However, I think it would be
strange for a library to enforce such a constraint at compile-time --
I agree that language support for CP should instead enforce this
constraint at compile-time.

Boost.Contract could be modified to enforce this constraint by
removing the CONTRACT_ASSERT() macros. Would this complicate the macro
syntax even more?

    template<typename T>
    class myvector {

        CONTRACT_FUNCTION_DECL(
        (iterator) (erase)( (iterator)(first) (iterator)(last) ) (copyable)
            (postcondition) (result) ( // no `{` bracket
                ( size() == (CONTRACT_OLDOF(this)->size() -
std::distance(first, last) )
                ( if (empty()) (result == end()) ) // if-guarded condition
            ) // no `}` braket
        ...
        )

        ...
    };

Note how the postconditions are just a preprocessor sequence of
boolean expressions asserting the contract. The if-guarded conditions
can AND (&&) multiple assertions plus they can list an optional 3rd
element for the else block, for example:

    (precondition) (
        (if (check)
            ( then1 && then2 )
        else
            ( else1 && else 2 )
        ) // endif
    )

If check is true then then1 and then2 conditions are asserted, else
else1 and else2 conditions are asserted.

4) BODY KEYWORD
n1962 does not use the body keyword. Instead, Boost.Contract macros use (body).

Boost.Contract could be changed to remove the need for (body) -- the
body will simply be the last element in the contract sequence.

This way, and removing also the CONTRACT_ASSERT(), Boost.Contract
syntax will be _exactly_ the same as n1962 with the "only" addition of
the () preprocessor wrappings:

    template<typename T> // n1962 syntax
    class myvector {

        void push_back(const T& element)
            precondition {
                size() < max_size();
            }
            postcondition {
                back() == element;
                size() == (oldof size() + 1);
            }
        {
            vector_.push_back(element);
        }

        ...
    };

    template<typename T> // Boost.Contract syntax
    class myvector {

        CONTRACT_FUNCTION_DECL(
        (void) (push_back)( (const T&)(element) ) (copyable)
            (precondition) ( // no CONTRACT_ASSERT()
                ( size() < max_size() )
            )
            (postcondition) (
                ( back() == element )
                ( size() == (CONTRACT_OLDOF(this)->size() + 1) )
            )
        ({ // no (body)
            vector_.push_back(element);
        }) )

        ...
    };

Is the macro syntax more readable with or without (body) and/or
CONTRACT_ASSERT()?

5) CONTRACT CHECKING ORDER (policy)
n1962 checks contracts as pre > inv > body > inv > post. Instead,
Boost.Contract checks contracts as inv > pre > body > inv > post,
where inv is static-inv > non-static-inv.

Note that Boost.Contract checks class invariants before preconditions
while n1962 does not.

However, n1962 footnote [9] says ``Strictly speaking the invariant
needs to hold before the precondition is executed because the
contracts might call public functions of the class which require the
invariant to be established. Currently we do not expect that to be a
practical problem though, and the current specification is easier to
implement.''. In addition, if invariants are checked first programmers
can assert pre/postconditions assuming the class invariants are true
(furthermore, non-static class invariants can be programmed assuming
static class invariants are true). For example, if the class
invariants were to assert a member pointer to be not null, both
pre/postconditions can assert conditions on this pointer without
checking for nullity first.

Therefore, I concluded Boost.Contract inv > pre is a preferred
approach over n1962 pre > inv. However, Boost.Contract could be
changed to check preconditions before invariants to comply with n1962.

6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy)
n1962 only disables assertion checking from within preconditions
checking. Instead, Boost.Contract disables assertion checking from
within all contract checking.

I found this policy useful to prevent infinite recursion. Previous
revisions of n1962 (n1613) specified the same policy implemented by
Boost.Contract. Furthermore, Eiffel implements the Boost.Contract
policy. Boost.Contract could be changed to comply with n1962.

Why does n1962 disable assertion checking only from within preconditions?

7) NESTED FUNCTION CALLS (policy)
n1962 disable nothing. Instead, Boost.Contract disables invariant
checking within nested function calls.

I found this policy useful to prevent infinite recursion. Previous
revisions of n1962 (n1613) specified the Boost.Contract policy. Eiffel
disables all checks (not just invariants). Boost.Contract could be
changed to comply with n1962.

Why does n1962 not disable invariants checking in nested calls?

8) CODE ORDERING
Both n1962 and Boost.Contract require preconditions > postconditions >
body to be specified in this order. Instead, Eiffel uses preconditions
...
body > postconditions.
People new to CP usually ask why the order is not pre > body > post
when looking at the contracts for the 1st time. However, after using
the library, the same people appreciate pre > post > body more because
the programming is cleaner "first program the contracts (pre and post)
then the body". I think using only one ordering is better to enforce
code consistency and I prefer pre > post > body over Eiffel's pre >
body > post.

Do you think Boost.Contract should be modified to support both n1962
and Eiffel orderings?

9) LOOP VARIANTS
n1962 does not support loop variants. Instead, Boost.Contract supports
loop variants with semantics similar to Eiffel's loop variants.

I find loop variants not useful in practice so I do not think I would
personally recommend them for language support. However, it was easy
enough to add them to Boost.Contract and I would leave them in the
library.

10) FAILURE HANDLERS
In n1962 section 4.6: <<The precondition for all the set_XX_handler
functions should be r != 0>>. Instead, Boost.Contract behaviour is
undefined if a null handler function pointer `r` is specified.

Boost.Contract mirrors the C++ specifications for std::set_terminate()
which indicates undefined behaviour if a null terminate handler
function pointer is specified. This could be changed.

11) OLDOF
n1962 allows to apply oldof to *any expression* that can be copied.
Instead, Boost.Contract only supports CONTRACT_OLDOF() for *object and
the function parameters* that can be copied.

This is a limitation of Boost.Contract because, for example, in order
to get the old value of a vector size I need to copy the entire vector
adding more overhead respect to copying just the vector size (which is
simply an integer):

    oldof vector.size() // n1962: Just copy the integer size().
    CONTRACT_OLDOF(vector).size() // Boost.Contract: Copy entire vector...

Furthermore, if the vector object cannot be copied, I cannot not get
its old size even if the size itself can be copied because it is just
an integer:

    oldof noncopyable_vector.size() // n1962: OK, just copy the integer size().
    CONTRACT_OLDOF(noncopyable_vector).size() // Boost.Contract:
Cannot do this because cannot copy noncopyable_vector...

Finally, the use of CONTRACT_OLDOF(variable) requires programmers to
explicitly indicate that the variable type is copyable using
(copyable) in the function signature adding syntactic overhead.

Unfortunately, I do not know how to remove these library limitations.
(All of that said, Boost.Contract old value support is very useful and
it successfully covered all the uses cases and examples presented in
n1962 and in a number of C++/Eiffel books/articles.)

12) CONSTANT-CORRECTNESS
Block invariants are constant-correct in n1962 but not in
Boost.Contract. (Class invariants and pre/postconditions are
constant-correct in both n1962 and Boost.Contract.)

Unfortunately, I do not know how to enforce constant-correctness of
block invariants (and also of loop variants) for Boost.Contract
because I cannot inject const within a code block:

    class z {
        void f() {
            const { // Can't do this... so f() is not const and block
invariants are also not const in this context...
                ... // block invariant here
            }
        }
    };

This is a limitation of Boost.Contract.

Regards,
Lorenzo

[boost] [contract] diff n1962

Lorenzo Caminiti