Hi, On Fri, Apr 9, 2010 at 2:00 AM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
From: "Lorenzo Caminiti" <lorcaminiti@gmail.com>
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