Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Thorsten Ottosen (nesotto_at_[hidden])
Date: 2010-04-09 07:57:10

Lorenzo Caminiti skrev:
> 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?

I investigated a large Eiffel library and found that the feature wasn't 
really used. I could come up with zero /realistic/ use-cases, and so we
thought it was better to leave it out.

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

It never occurred to us that (subsets of) global variables
should have their own invariant. Again, how common is this?

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

yeah, every keyword costs you a kidney. :-)

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

I think what is needed is a dead-good realistic example from real
code. In some sense the initial check for the invariant is
redundant, because it will always have been performed in the constructor 
or at the end of a nother function. We have it there as an additional
debugging help, nothing else.

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

You got it the wrong way. Preconditions /never/ disable anything.
You can prove that if you do so, an incorrect parameter might
be passed on to the function body.

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

Because the callee does not know if the invariant has been
proper established by the caller. The caller cares about the invariant
on entrance/exit, but now must also do so when calling another
public function.

HTH

-Thorsten