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