Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: vicente.botet (vicente.botet_at_[hidden])
Date: 2010-04-09 02:00:22

----- Original Message ----- 
From: "Lorenzo Caminiti" <lorcaminiti_at_[hidden]>
To: <boost_at_[hidden]>
Sent: Friday, April 09, 2010 1:26 AM
Subject: [boost] [contract] diff n1962

> 
> Hello all,

Hi Lorenzo,
 
> 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.

Excelent idea. This comparation is very useful. 
 
> 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? 
 
> 
> 
> 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.
 
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
> 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()?

I find it closer to the C++ syntax in N1962 and find a big improvement respect to the previous proposal.
 
> 
> 
> 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?

Is there any reason to to disable them. COuld you elaborate which invariants checking  Boost.Contract  is disabling?
 
> 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?

No. I think you need to provide just one ordering, and why not the N1962 ordering.
 
> 
> 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.)

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);
        }) )
 
 
Best,
Vicente