----- Original Message ----- From: "Lorenzo Caminiti" <lorcaminiti@gmail.com> To: <boost@lists.boost.org> 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