Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-11 21:59:46

Hi,

On Fri, Apr 9, 2010 at 2:00 AM, vicente.botet <vicente.botet_at_[hidden]> wrote:
> From: "Lorenzo Caminiti" <lorcaminiti_at_[hidden]>
>> 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.>>.
>
> The contract of the overrriding function must be weaker than the overrided one. How can this been ensured otherwise?

>From n1613 section 2: <<It is possible to formalize the notion of
overriding a virtual function;
the idea can be justified by substitution principles and is referred to as
subcontracting. Subcontracting consists of two simple rules that the
overriding function must obey [Mey97]. (1) the precondition cannot
be stronger, and (2) the postcondition cannot be weaker. ...
Thus the compiler will automatically OR preconditions from the base
class function with the preconditions of the overriding function and it
will automatically AND postconditions from the base class function
with the postconditions of the overriding function.>>.

Therefore, Boost.Contract checks preconditions of an overriding
function in short-circuit OR with the preconditions of all overridden
functions (that have a contract), following the inheritance order in
case of multiple inheritance. Class invariants (static and non) and
postconditions are instead checked in short-circuit AND. This ensures
that everywhere a callers is calling x::f() satisfying its contract,
it can also call y::f() is y inherits from x (the substitution
principle).

That is because however you program y::f() and its contract, x::f()
preconditions are inherited in OR so a callers satisfying x::f() will
also satisfy y::f() preconditions. Furthermore, a caller expecting
x::f() postconditions to be satisfied will find that true also when
calling y::f() because postcondition are inherited in AND (same story
for invariants). Therefore, from the caller's prospective a call to
x::f() from a context in which x::f() contract holds can be replaced
(or "substituted") with a call to y::f() without braking the contract
(i.e., substitution principle).

>> 3) ARBITRARY CODE IN CONTRACTS
> I don't find
>
>  ( size() == (OLDOF(this)->size() - std::distance(first, last) )
>  ( if (empty()) (result == end()) )
>
> more complicated than
>
>  ASSERT( size() == (OLDOF(this)->size() - std::distance(first, last) );
>  if (empty()) ASSERT(result == end());
>
> Even if the last one can be clearest as more explicit and use the usual sentence.
>
>> 4) BODY KEYWORD
> I find it closer to the C++ syntax in N1962 and find a big improvement respect to the previous proposal.

Yes, I am also leaning toward this syntax plus generating the function
signature automatically for CONTRACT_FUNCTION() but repeating the
class signature for CONTRACT_CLASS() (to avoid the single line class
definition issue). I think I will also provide Boost.Concept support
via a (requires)( (Concept1) (Concept2) ... ) block after
(template)(...) (mirroring ConceptC++ syntax).

>> 6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy)
>> 7) NESTED FUNCTION CALLS (policy)
> Is there any reason to to disable them. COuld you elaborate which invariants checking  Boost.Contract  is disabling?

As I mentioned in a separate email, I will provide examples for 6) and
7) so we can discuss in concrete.

>> 8) CODE ORDERING
> No. I think you need to provide just one ordering, and why not the N1962 ordering.

This is also the ordering I prefer. I will leave it this way.

>> 11) OLDOF
> I don't know if the following could be considered as an optimization approach.
> The contract function declaration could add a list of variables storing the old values of the required espressions.
> For example if the postcondition will check for size() == (oldof(size()) + 1), we can store in a variable old_size the size before calling.
>
>        CONTRACT_FUNCTION_DECL(
>        (void) (push_back)( (const T&)(element) ) ((old_size) (size()))
>            (precondition) (
>                ( size() < max_size() )
>            )
>            (postcondition)
>                ( back() == element )
>                ( size() == (old_size + 1) )
>            )
>        ({
>            vector_.push_back(element);
>        }) )

I think this is possible (you might need to also specify the type of
the expression, Boost.Typeof might be of help). However, it will
complicate the syntax even more... even if I mentioned a few
limitations of Boost.Contract oldof implementation, I must say that
CONTRACT_OLDOF() was good and simple enough to handle all the many
examples that I have encountered.

Therefore, I do not think I will implement this suggestion unless
people indicate it is truly needed. (I am still trying to eliminate
(copyable) and relax the other CONTRACT_OLDOF() constraints
essentially by trying to have the library do what you suggest here but
automatically without programmers entering extra tokens in the
contract signature -- it is NOT looking good... I can't really
metaprogram that...)

Note: The copy overhead can be disabled in production code by
disabling postconditions checking all together (postconditions will
rarely be enable in production releases because they can be expensive
to evaluate and they check implementation correctness so they are
mainly useful during testing as discussed by [Meyer1997] and many
others).

Thanks a lot for the comments.
Lorenzo