[contract] diff n1962
Hello all, 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. 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.>>. 2) STATIC CLASS INVARIANTS n1962 does not support static class invariants. Instead, Boost.Contract supports static class invariants. Non-static class invariants are not checked at constructor entry, at destructor exit, and at entry/exit of static member functions (because there is no object in these cases). Static class invariants instead are always checked at entry/exit of constructors, destructor, and (static or non-static) member functions. I added static class invariants for completeness. Boost.Contract could drop static class invariants to comply with n1962 (but I find them useful). struct z { static int counter; int number; CONTRACT_CLASS( (z) (static) (invariant) ({ // Static class invariants (no object here). CONTRACT_ASSERT( counter >= 0 ); }) (invariant) ({ // Non-static class invariants (`this` present). CONTRACT_ASSERT( number <= counter ); }) ) ... }; Why does n1962 not support static class invariants? 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. 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()? 5) CONTRACT CHECKING ORDER (policy) n1962 checks contracts as pre > inv > body > inv > post. Instead, Boost.Contract checks contracts as inv > pre > body > inv > post, where inv is static-inv > non-static-inv. Note that Boost.Contract checks class invariants before preconditions while n1962 does not. However, n1962 footnote [9] says ``Strictly speaking the invariant needs to hold before the precondition is executed because the contracts might call public functions of the class which require the invariant to be established. Currently we do not expect that to be a practical problem though, and the current specification is easier to implement.''. In addition, if invariants are checked first programmers can assert pre/postconditions assuming the class invariants are true (furthermore, non-static class invariants can be programmed assuming static class invariants are true). For example, if the class invariants were to assert a member pointer to be not null, both pre/postconditions can assert conditions on this pointer without checking for nullity first. Therefore, I concluded Boost.Contract inv > pre is a preferred approach over n1962 pre > inv. However, Boost.Contract could be changed to check preconditions before invariants to comply with n1962. 6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking. I found this policy useful to prevent infinite recursion. Previous revisions of n1962 (n1613) specified the same policy implemented by Boost.Contract. Furthermore, Eiffel implements the Boost.Contract policy. Boost.Contract could be changed to comply with n1962. Why does n1962 disable assertion checking only from within preconditions? 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? 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? 9) LOOP VARIANTS n1962 does not support loop variants. Instead, Boost.Contract supports loop variants with semantics similar to Eiffel's loop variants. I find loop variants not useful in practice so I do not think I would personally recommend them for language support. However, it was easy enough to add them to Boost.Contract and I would leave them in the library. 10) FAILURE HANDLERS In n1962 section 4.6: <<The precondition for all the set_XX_handler functions should be r != 0>>. Instead, Boost.Contract behaviour is undefined if a null handler function pointer `r` is specified. Boost.Contract mirrors the C++ specifications for std::set_terminate() which indicates undefined behaviour if a null terminate handler function pointer is specified. This could be changed. 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.) 12) CONSTANT-CORRECTNESS Block invariants are constant-correct in n1962 but not in Boost.Contract. (Class invariants and pre/postconditions are constant-correct in both n1962 and Boost.Contract.) Unfortunately, I do not know how to enforce constant-correctness of block invariants (and also of loop variants) for Boost.Contract because I cannot inject const within a code block: class z { void f() { const { // Can't do this... so f() is not const and block invariants are also not const in this context... ... // block invariant here } } }; This is a limitation of Boost.Contract. Regards, Lorenzo
----- 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
Lorenzo Caminiti skrev:
Hello all,
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.
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?
I investigated a large Eiffel library and found that the feature wasn't really used. I could come up with zero /realistic/ use-cases, and so we thought it was better to leave it out.
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.>>.
2) STATIC CLASS INVARIANTS n1962 does not support static class invariants. Instead, Boost.Contract supports static class invariants.
Non-static class invariants are not checked at constructor entry, at destructor exit, and at entry/exit of static member functions (because there is no object in these cases). Static class invariants instead are always checked at entry/exit of constructors, destructor, and (static or non-static) member functions.
I added static class invariants for completeness. Boost.Contract could drop static class invariants to comply with n1962 (but I find them useful).
struct z { static int counter; int number;
CONTRACT_CLASS( (z) (static) (invariant) ({ // Static class invariants (no object here). CONTRACT_ASSERT( counter >= 0 ); }) (invariant) ({ // Non-static class invariants (`this` present). CONTRACT_ASSERT( number <= counter ); }) )
... };
Why does n1962 not support static class invariants?
It never occurred to us that (subsets of) global variables should have their own invariant. Again, how common is this?
4) BODY KEYWORD n1962 does not use the body keyword. Instead, Boost.Contract macros use (body).
yeah, every keyword costs you a kidney. :-)
5) CONTRACT CHECKING ORDER (policy) n1962 checks contracts as pre > inv > body > inv > post. Instead, Boost.Contract checks contracts as inv > pre > body > inv > post, where inv is static-inv > non-static-inv.
Note that Boost.Contract checks class invariants before preconditions while n1962 does not.
However, n1962 footnote [9] says ``Strictly speaking the invariant needs to hold before the precondition is executed because the contracts might call public functions of the class which require the invariant to be established. Currently we do not expect that to be a practical problem though, and the current specification is easier to implement.''. In addition, if invariants are checked first programmers can assert pre/postconditions assuming the class invariants are true (furthermore, non-static class invariants can be programmed assuming static class invariants are true). For example, if the class invariants were to assert a member pointer to be not null, both pre/postconditions can assert conditions on this pointer without checking for nullity first.
I think what is needed is a dead-good realistic example from real code. In some sense the initial check for the invariant is redundant, because it will always have been performed in the constructor or at the end of a nother function. We have it there as an additional debugging help, nothing else.
6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking.
I found this policy useful to prevent infinite recursion. Previous revisions of n1962 (n1613) specified the same policy implemented by Boost.Contract. Furthermore, Eiffel implements the Boost.Contract policy. Boost.Contract could be changed to comply with n1962.
Why does n1962 disable assertion checking only from within preconditions?
You got it the wrong way. Preconditions /never/ disable anything. You can prove that if you do so, an incorrect parameter might be passed on to the function body.
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?
Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function. HTH -Thorsten
AMDG Lorenzo Caminiti wrote:
struct z { static int counter; int number;
CONTRACT_CLASS( (z) (static) (invariant) ({ // Static class invariants (no object here). CONTRACT_ASSERT( counter >= 0 ); }) (invariant) ({ // Non-static class invariants (`this` present). CONTRACT_ASSERT( number <= counter ); }) )
... };
Why does n1962 not support static class invariants?
Would it be possible to have something like CONTRACT_INVARIANT { // arbitrary code }; CONTRACT_STATIC_INVARIANT { // arbitrary code }; To me at least, this would look cleaner than having all the parentheses.
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.
This kind of worries me. Do you always make a copy whether it's needed or not when the object is marked as copiable?
12) CONSTANT-CORRECTNESS Block invariants are constant-correct in n1962 but not in Boost.Contract. (Class invariants and pre/postconditions are constant-correct in both n1962 and Boost.Contract.)
Unfortunately, I do not know how to enforce constant-correctness of block invariants (and also of loop variants) for Boost.Contract because I cannot inject const within a code block:
class z { void f() { const { // Can't do this... so f() is not const and block invariants are also not const in this context... ... // block invariant here } } };
This is a limitation of Boost.Contract.
You can pull the code block out into a separate function. In Christ, Steven Watanabe
Hello all, On Thu, Apr 8, 2010 at 7:26 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
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.
Thank you very much for all your replies. I will address your comments and modify Boost.Contract as needed. Before that however, I have one additional question on constructors -- for everyone and again especially for the n1962 authors. CONSTRUCTORS Does n1962 require constructor preconditions to be checked before or after the execution of the member initialization list?
From n1962 section 4.2.2: <<Constructors behave much like member functions. This means that a constructor can have a precondition and a postcondition. The precondition may not reference member variables.>>.
Boost.Contract checks preconditions after the member initialization: member-init > static-inv > pre > body > static-inv > inv > post. However, when asked why I could not really come up with an explanation but that it would be difficult to implement Boost.Contract differently... Eiffel checks "default" > pre > body > inv > post. Where "default" essentially means that member variables are in a default state. I think, this is similar to executing the member initialization before checking preconditions but not quite the same because default member values for Eiffel are essentially just Void. C++ instead can assign more complex values in the member initialization list. Because these values can be functions of the constructor input parameters, you can make the argument that C++ preconditions should be checked before the member initialization list so to validate the constructor parameters before they are used to initialize the members. Thank you. Lorenzo
----- Original Message ----- From: "Lorenzo Caminiti" <lorcaminiti@gmail.com> To: <boost@lists.boost.org> Sent: Sunday, April 11, 2010 4:16 PM Subject: Re: [boost] [contract] diff n1962 Hello all, On Thu, Apr 8, 2010 at 7:26 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
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.
Thank you very much for all your replies. I will address your comments and modify Boost.Contract as needed. Before that however, I have one additional question on constructors -- for everyone and again especially for the n1962 authors. CONSTRUCTORS Does n1962 require constructor preconditions to be checked before or after the execution of the member initialization list?
From n1962 section 4.2.2: <<Constructors behave much like member functions. This means that a constructor can have a precondition and a postcondition. The precondition may not reference member variables.>>.
Boost.Contract checks preconditions after the member initialization: member-init > static-inv > pre > body > static-inv > inv > post. However, when asked why I could not really come up with an explanation but that it would be difficult to implement Boost.Contract differently... Eiffel checks "default" > pre > body > inv > post. Where "default" essentially means that member variables are in a default state. I think, this is similar to executing the member initialization before checking preconditions but not quite the same because default member values for Eiffel are essentially just Void. C++ instead can assign more complex values in the member initialization list. Because these values can be functions of the constructor input parameters, you can make the argument that C++ preconditions should be checked before the member initialization list so to validate the constructor parameters before they are used to initialize the members. Thank you. Lorenzo _______________________________________________ Hi Lorenzo, I supose that the constructor preconditions are evaluated before the member initialization as this initialization can rely on the preconditions been satisfied. Note also that preconditions/postconditions must to be in the declaration part, and the member initialization is on the definition part. I understand that it is not easy for Boost.Contract to check the precondition before member initialization . To be able to do that you will need to have a first member or inherit from a 'precondition' class that do this precondition check, class C : C_constructor_precondition ... { C(T1 p1) : C_constructor_precondition(p1), ... { // ... } }; but this seems to me a severe constraint and adds more complexity. I think that I can live with preconditions check after member initialization. Best, _____________________ Vicente Juan Botet Escribá http://viboes.blogspot.com/
----- Original Message ----- From: "Steven Watanabe" <watanabesj@gmail.com> To: <boost@lists.boost.org> Sent: Saturday, April 10, 2010 5:49 PM Subject: Re: [boost] [contract] diff n1962
AMDG
Lorenzo Caminiti wrote:
struct z { static int counter; int number;
CONTRACT_CLASS( (z) (static) (invariant) ({ // Static class invariants (no object here). CONTRACT_ASSERT( counter >= 0 ); }) (invariant) ({ // Non-static class invariants (`this` present). CONTRACT_ASSERT( number <= counter ); }) )
... };
Why does n1962 not support static class invariants?
Would it be possible to have something like CONTRACT_INVARIANT { // arbitrary code }; CONTRACT_STATIC_INVARIANT { // arbitrary code };
To me at least, this would look cleaner than having all the parentheses.
I think that the major problem with this approach is that is no simple to inhibit the CP code when we don't want to include it. Boost.Contract defines a members in the class check the contract state. We could have a macro for that #if defined CONTRACT_CHECK_CLASS_INVARIANT || \ defined CONTRACT_CHECK_PRECONDITION || \ defined CONTRACT_CHECK_POSTCONDITION #define BOOST_CONTRACT_STATE \ friend class contract::state; \ mutable contract::state contract_state_; #else #define BOOST_CONTRACT_STATE #endif // contracts The library can provide also these macros #define BOOST_CONTRACT_CLASS_STATIC_INVARIANT \ static void contract_static_invariant_() #define BOOST_CONTRACT_CLASS_INVARIANT \ static void contract_invariant_() Then we can do struct z { static int counter; int number; BOOST_CONTRACT_STATE // (*) #if defined CONTRACT_CHECK_CLASS_INVARIANT // (*) CONTRACT_INVARIANT { CONTRACT_ASSERT( counter >= 0 ); } CONTRACT_STATIC_INVARIANT { CONTRACT_ASSERT( number <= counter ); } #endif // (*) ... }; Note the added lines with (*). Do you think this is satisfactory?
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.
This kind of worries me. Do you always make a copy whether it's needed or not when the object is marked as copiable?
What do you think of storing in specific variables the old values and use them on the post condition. (postcondition)((old_size) (this)->size())) ({ CONTRACT_ASSERT( size() == (old_size + 1) ); }) This has the advantage that only the used old values are copied. Do you see another alternative?
12) CONSTANT-CORRECTNESS Block invariants are constant-correct in n1962 but not in Boost.Contract. (Class invariants and pre/postconditions are constant-correct in both n1962 and Boost.Contract.)
Unfortunately, I do not know how to enforce constant-correctness of block invariants (and also of loop variants) for Boost.Contract because I cannot inject const within a code block:
class z { void f() { const { // Can't do this... so f() is not const and block invariants are also not const in this context... ... // block invariant here } } };
This is a limitation of Boost.Contract.
You can pull the code block out into a separate function.
Yes as Steven says, you can always define a function with the needed const qualifiers that checks for the block invariant. But IMHO this complicates things a lot. I don't think that I will use these kind of functions so help to ensure that Block invariants are constant-correct. This could be a minor and aceptable limitation of a library solution. Best, _____________________ Vicente Juan Botet Escribá http://viboes.blogspot.com/
Hello, On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
Lorenzo Caminiti skrev:
1) SUBCONTRACTING n1962 allows only the base class to specify preconditions. Instead, Boost.Contract allows also derived classes to specify preconditions. ... Why does n1962 allow preconditions only for the base classes? ... I investigated a large Eiffel library and found that the feature wasn't really used. I could come up with zero /realistic/ use-cases, and so we thought it was better to leave it out.
This is an example of how overriding preconditions allows relaxed_name_list::put() to relax his parent's name_list::put() constraint that names cannot be duplicated in the list: http://dbcpp.sourceforge.net/example/Mitchell2002/name_list/names.hpp However, this is an academic example and not a realistic one. While I think it is conceivable some programmers would actually want to override preconditions, I cannot offer any realistic example -- within the ~60,000 lines of C++ project I work one, we essentially never used this feature. That said, I would leave this feature in Boost.Contract so people can experiment with it -- and perhaps come up with a realistic use case. I do understand the importance of a realistic use case if this feature were to be added for language support.
2) STATIC CLASS INVARIANTS n1962 does not support static class invariants. Instead, Boost.Contract supports static class invariants. ... Why does n1962 not support static class invariants? ... It never occurred to us that (subsets of) global variables should have their own invariant. Again, how common is this?
Also for this feature I cannot provide any realistic use case. In the ~60,000 lines of C++ project I work one, we never use static class invariants -- but we never even use static variables neither, we only use static const variables, so I am not sure how much can be concluded from that. Again, I would leave static class invariants in Boost.Contract for people to experiment with it (but I understand the need for real use cases if this were to be requested for language support).
5) CONTRACT CHECKING ORDER (policy) n1962 checks contracts as pre > inv > body > inv > post. Instead, Boost.Contract checks contracts as inv > pre > body > inv > post, where inv is static-inv > non-static-inv. ... I think what is needed is a dead-good realistic example from real code. In some sense the initial check for the invariant is redundant, because it will always have been performed in the constructor or at the end of a nother function. We have it there as an additional debugging help, nothing else.
Yes, but private member functions (and in case of Boost.Contract any member function, including public ones, without a contract) could have broken the invariant making the extra debugging invariant check even more useful. There might be a real example of this in the ~60,000 lines of C++ project I work one... it is a difficult analysis to conduct but I will keep an eye open for it.
6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking. ... Why does n1962 disable assertion checking only from within preconditions? ... You got it the wrong way. Preconditions /never/ disable anything. You can prove that if you do so, an incorrect parameter might be passed on to the function body.
Yes, I see that now -- from n1962 section 11 <<disabling of checks during assertions ... yes, but not in preconditions>>. Good thing I checked... Eiffel disables checks also in preconditions to avoid infinite recursion. I can change this in Boost.Contract but is there a concern with infinite recursion?
7) NESTED FUNCTION CALLS (policy) n1962 disable nothing. Instead, Boost.Contract disables invariant checking within nested function calls. ... Why does n1962 not disable invariants checking in nested calls? ... Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function.
I am not sure I understand, could you please provide an example? Similar to 6), Eiffel disables all checks in nested calls to avoid infinite recursion. Once I understand this better, I could change this in Boost.Contract but is there a concern with infinite recursion?
HTH
Yes, your comments as well as n1962 and all your previous CP proposal revisions have been of great help. Thank you very much. Lorenzo
----- Original Message ----- From: "Lorenzo Caminiti" <lorcaminiti@gmail.com> To: <boost@lists.boost.org> Sent: Monday, April 12, 2010 1:23 AM Subject: Re: [boost] [contract] diff n1962
6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking. ... Why does n1962 disable assertion checking only from within preconditions? ... You got it the wrong way. Preconditions /never/ disable anything. You can prove that if you do so, an incorrect parameter might be passed on to the function body.
Yes, I see that now -- from n1962 section 11 <<disabling of checks during assertions ... yes, but not in preconditions>>. Good thing I checked...
Eiffel disables checks also in preconditions to avoid infinite recursion. I can change this in Boost.Contract but is there a concern with infinite recursion?
7) NESTED FUNCTION CALLS (policy) n1962 disable nothing. Instead, Boost.Contract disables invariant checking within nested function calls. ... Why does n1962 not disable invariants checking in nested calls? ... Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function.
I am not sure I understand, could you please provide an example?
Similar to 6), Eiffel disables all checks in nested calls to avoid infinite recursion. Once I understand this better, I could change this in Boost.Contract but is there a concern with infinite recursion?
I don't see any problem with infinite recursion. Could you give an example? _____________________ Vicente Juan Botet Escribá http://viboes.blogspot.com/
On Sun, Apr 11, 2010 at 7:32 PM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking. ... Why does n1962 disable assertion checking only from within preconditions? ... You got it the wrong way. Preconditions /never/ disable anything. You can prove that if you do so, an incorrect parameter might be passed on to the function body.
Yes, I see that now -- from n1962 section 11 <<disabling of checks during assertions ... yes, but not in preconditions>>. Good thing I checked...
Eiffel disables checks also in preconditions to avoid infinite recursion. I can change this in Boost.Contract but is there a concern with infinite recursion?
7) NESTED FUNCTION CALLS (policy) n1962 disable nothing. Instead, Boost.Contract disables invariant checking within nested function calls. ... Why does n1962 not disable invariants checking in nested calls? ... Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function.
I am not sure I understand, could you please provide an example?
Similar to 6), Eiffel disables all checks in nested calls to avoid infinite recursion. Once I understand this better, I could change this in Boost.Contract but is there a concern with infinite recursion?
I don't see any problem with infinite recursion. Could you give an example?
Agreed: the most constructive way to discuss policies 6) and 7) is for me to present examples. I will work on this. (There were a couple of infinite recursion examples I encountered while reading CP Eiffel code and developing the library, I will dig that code up.) Lorenzo
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
Hello, On Sun, Apr 11, 2010 at 12:35 PM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
From: "Steven Watanabe" <watanabesj@gmail.com>
Would it be possible to have something like CONTRACT_INVARIANT { // arbitrary code }; CONTRACT_STATIC_INVARIANT { // arbitrary code };
To me at least, this would look cleaner than having all the parentheses.
I think that the major problem with this approach is that is no simple to inhibit the CP code when we don't want to include it. Boost.Contract defines a members in the class check the contract state. We could have a macro for that
This is possible, in fact you could use `void contract_invariant_() const {...}` directly without any macro (the state, class type, etc will eventually remain in CONTRACT_CLASS( (class-type) (base-type1) (base-type2) ... )). However, this has the following drawbacks: 1) As indicated by Vicente programmers will have to add the #ifdef to remove contract code when invariants are not checked. However, it was proposed by Andrzej to always leave contract code there so it is compiled and checked syntactically (this could be implemented in the future) -- Boost.Contract will not execute invariant checking at run-time when CONTRACT_CHECK_CLASS_INVARIANT is #undef anyway. 2) However, this is NOT possible for member functions because they have result value and arguments. Therefore, CONTRACT_FUNCTION() will need to use the parenthesis for (precondition) and (postcondition). Given that, I think it is better for the library to provide a consistent interface across both its macros CONTRACT_FUNCTION() and CONTRACT_CLASS() therefore using (invariant). What do you think? Let me unveil the macro magic so this will become more clear: template<typename T> class myvector: public pushable<T> { CONTRACT_CLASS( (myvector) (pushable<T>) (invariant) ( ( (size() == 0) == empty() ) ) ) CONTRACT_FUNCTION( (void) (push_back)( (const T&)(element) ) (copyable) (precondition) ( ( size() < max_size() ) ) (postcondition) ( ( size() == (CONTRACT_OLDOF(this)->size() + 1) ) ) ({ vector_.push_back(element); }) ) ... }; Expands to code equivalent to: template<typename T> class myvector: public pushable<T> { // CONTRACT_CLASS() expands to: typedef myvector contract_class_type_; typedef pushable<T> contract_base_type0_; friend class contract::state; mutable contract::state contract_state; static void contract_static_invariant_() { // (1) } void contract_invariant_() const { // (2) if (!((size() == 0) == empty())) throw contract::failure(__FILE__, __LINE__, "(size() == 0) == empty()"); } // CONTRACT_FUNCTION expands to: public: void push_back(const T& element) { contract_push_back_element_().call(this, element); } private: void contract_precondition_push_back_element_(const T& element) const { ... // preconditions throwing contract::failure() } private: void contract_postcondition_push_back_element_( // (3) const contract_class_type* old_this, // old value for object this const T& element, contract::noold // no old value for element ) const { ... // postconditions throwing contract::failure() } protected: void contract_body_push_back_(const T& element) { // (4) vector_.push_back(element); } protected: struct contract_push_back_element_: contract::nonstatic_member_function< void (contract::copyable<contract_class_type>*, const T&), // contracted member function type contract_base_type::contract_push_back_element_> { // subcontracting contract_push_back_element_(): contract::nonstatic_member_function< void (contract::copyable<contract_class_type>*, const T&), contract_base_type::contract_push_back_element_>( &class_type::contract_body_push_back, &class_type::contract_precondition_push_back_element_, &class_type::contract_postcondition_push_back_element) {} }; public: ... }; (For simplicity, I left out #ifdef for optional contract compilation, introspection code to determine base class from which to subcontract, and original type vs. noold type selection based on copyable<> type tag.) You can see that (1) and (2) can easily be pulled out from CONTRACT_CLASS() as you suggested. However, pulling out (3) and (4) from CONTRACT_FUNCTION() will require programmers to repeat the contracted function arguments in (3) and (4), plus the original type or noold for the relative oldof values in (4), plus the eventual result value as an extra parameter of (4) (not present in this example). That will be a lot of code to program and it would not be much different than requiring to program the entire expanded code above. BTW, the code above is part of Boost.Contract public API and programmers can always use it if they do not want to use the macros (but that's a lot of setup code to write...). For consistency, I think that if (precondition) and (postcondition) are part of CONTRACT_FUNCTION() then (invariant) should be kept in CONTRACT_CLASS().
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.
This kind of worries me. Do you always make a copy whether it's needed or not when the object is marked as copiable?
However, why does this worry you? If programmers do not need CONTRACT_OLDOF() then they simply do not tag the type (copyable) and there is no overhead. Note that the (copyable) is used within the function contract, so the object can be (and should be) tagged (copyable) only for the member functions that use CONTRACT_OLDOF(this). Let me explain: 1) Yes, Boost.Contract always makes a copy whether it is needed of not for object and arguments that are tagged (copyable). 2) Boost.Contract documentation explains that programmers should tag a type (copyable) only when (a) the relative variable old value CONTRACT_OLDOF(variable-name) is used in postconditions and (b) the type has a constant correct copy constructor. 3) Boost.Contract will generate a compile-time error if CONTRACT_OLDOF() is used on a variable not tagged (copyable) and/or the tagged type does not have the constant-correct copy constructor. 4) Boost.Contract cannot detect if a variable tagged (copyable) is not used in postconditions by CONTRACT_OLDOF() in which case the copy and relative run-time overhead will be wasted. Ideally, Boost.Contract will be able to automatically detect if CONTRACT_OLDOF(variable-name) is used in postconditions, then tag the related type (copyable) at compile-time, and therefore make the copy at run-time. This is exactly why I was asking if is_macro_called() can be implemented but it seems that it is not possible...
What do you think of storing in specific variables the old values and use them on the post condition. (postcondition)((old_size) (this)->size())) ({ CONTRACT_ASSERT( size() == (old_size + 1) ); })
This has the advantage that only the used old values are copied. Do you see another alternative?
This option suggested by Vicente should be feasible but it complicates the syntax. (Eventually, I like the old variable to follow (postcondition) as suggested here instead that being after the function signature.)
12) CONSTANT-CORRECTNESS Block invariants are constant-correct in n1962 but not in Boost.Contract. (Class invariants and pre/postconditions are constant-correct in both n1962 and Boost.Contract.)
Unfortunately, I do not know how to enforce constant-correctness of block invariants (and also of loop variants) for Boost.Contract because I cannot inject const within a code block:
class z { void f() { const { // Can't do this... so f() is not const and block invariants are also not const in this context... ... // block invariant here } } };
This is a limitation of Boost.Contract.
You can pull the code block out into a separate function.
Yes as Steven says, you can always define a function with the needed const qualifiers that checks for the block invariant. But IMHO this complicates things a lot. I don't think that I will use these kind of functions so help to ensure that Block invariants are constant-correct. This could be a minor and aceptable limitation of a library solution.
One key issue is that is that the const function will have to offer all the original function arguments, plus local variables, etc because everything that is in scope can be used by BLOCK_INVARIANT() (in constant-correct context) to make the assertion: class x { void f(int a) { int b = a; CONTRACT_BLOCK_INVARIANT( a == b ); ... } ... }; How do I expand this to the separate const-correct function call? Of course programmers can manually program it: class x { void bool f_check1_(const int& a, const int& b) { return a == b; } void f(int a) { int b = a; CONTRACT_BLOCK_INVARIANT( f_check1_(a, b) ); ... } ... }; (I tried to do this with classes declared locally within f() where BLOCK_INVARIANT() is used but I was not able to get it to work because you still do not see the function arguments, local variables, outer object `this`, etc.) Thank you very much for your comments. Lorenzo
----- Original Message ----- From: "Lorenzo Caminiti" <lorcaminiti@gmail.com> To: <boost@lists.boost.org> Sent: Monday, April 12, 2010 5:27 AM Subject: Re: [boost] [contract] diff n1962 Hello, On Sun, Apr 11, 2010 at 12:35 PM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
From: "Steven Watanabe" <watanabesj@gmail.com>
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.
This kind of worries me. Do you always make a copy whether it's needed or not when the object is marked as copiable?
However, why does this worry you? If programmers do not need CONTRACT_OLDOF() then they simply do not tag the type (copyable) and there is no overhead. Note that the (copyable) is used within the function contract, so the object can be (and should be) tagged (copyable) only for the member functions that use CONTRACT_OLDOF(this). Let me explain: 1) Yes, Boost.Contract always makes a copy whether it is needed of not for object and arguments that are tagged (copyable). 2) Boost.Contract documentation explains that programmers should tag a type (copyable) only when (a) the relative variable old value CONTRACT_OLDOF(variable-name) is used in postconditions and (b) the type has a constant correct copy constructor. 3) Boost.Contract will generate a compile-time error if CONTRACT_OLDOF() is used on a variable not tagged (copyable) and/or the tagged type does not have the constant-correct copy constructor. 4) Boost.Contract cannot detect if a variable tagged (copyable) is not used in postconditions by CONTRACT_OLDOF() in which case the copy and relative run-time overhead will be wasted. Ideally, Boost.Contract will be able to automatically detect if CONTRACT_OLDOF(variable-name) is used in postconditions, then tag the related type (copyable) at compile-time, and therefore make the copy at run-time. This is exactly why I was asking if is_macro_called() can be implemented but it seems that it is not possible...
What do you think of storing in specific variables the old values and use them on the post condition. (postcondition)((old_size) (this)->size())) ({ CONTRACT_ASSERT( size() == (old_size + 1) ); })
This has the advantage that only the used old values are copied. Do you see another alternative?
This option suggested by Vicente should be feasible but it complicates the syntax. (Eventually, I like the old variable to follow (postcondition) as suggested here instead that being after the function signature.) _______________________________________________ VBE>I think that what worries Steven is that we need to state explicitly if a given variable must be copied. Maybe the library can provide a mode on which the copies are done always (maybe a trait class could be used to select which one must be copied), so no need to add the (copyable) tag. As post conditions are usualy evaluated only on debug mode, the performance degradation could be considered a minor drawback.
12) CONSTANT-CORRECTNESS Block invariants are constant-correct in n1962 but not in Boost.Contract. (Class invariants and pre/postconditions are constant-correct in both n1962 and Boost.Contract.)
Unfortunately, I do not know how to enforce constant-correctness of block invariants (and also of loop variants) for Boost.Contract because I cannot inject const within a code block:
class z { void f() { const { // Can't do this... so f() is not const and block invariants are also not const in this context... ... // block invariant here } } };
This is a limitation of Boost.Contract.
You can pull the code block out into a separate function.
Yes as Steven says, you can always define a function with the needed const qualifiers that checks for the block invariant. But IMHO this complicates things a lot. I don't think that I will use these kind of functions so help to ensure that Block invariants are constant-correct. This could be a minor and aceptable limitation of a library solution.
One key issue is that is that the const function will have to offer all the original function arguments, plus local variables, etc because everything that is in scope can be used by BLOCK_INVARIANT() (in constant-correct context) to make the assertion: class x { void f(int a) { int b = a; CONTRACT_BLOCK_INVARIANT( a == b ); ... } ... }; How do I expand this to the separate const-correct function call? Of course programmers can manually program it: class x { void bool f_check1_(const int& a, const int& b) { return a == b; } void f(int a) { int b = a; CONTRACT_BLOCK_INVARIANT( f_check1_(a, b) ); ... } ... }; (I tried to do this with classes declared locally within f() where BLOCK_INVARIANT() is used but I was not able to get it to work because you still do not see the function arguments, local variables, outer object `this`, etc.) _______________________________________________ VBE> Boost.ScopeExit showed a technique that can be used to emulate local functions. Alexander proposed long time ago to provide it independently from ScopeExit but to my knowledge this has not been done. Using this technique Boost.Contract could try to emulate a const function, but I think yet that compicates the syntax for not too much user advantage. _____________________ Vicente Juan Botet Escribá http://viboes.blogspot.com/
Lorenzo Caminiti skrev:
Hello all,
On Thu, Apr 8, 2010 at 7:26 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
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.
Thank you very much for all your replies. I will address your comments and modify Boost.Contract as needed. Before that however, I have one additional question on constructors -- for everyone and again especially for the n1962 authors.
CONSTRUCTORS Does n1962 require constructor preconditions to be checked before or after the execution of the member initialization list?
Maybe the paper is not as clear as it could be, but the intend is *before* the member initializer list. -Thorsten
On Mon, Apr 12, 2010 at 7:05 AM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
Lorenzo Caminiti skrev:
CONSTRUCTORS Does n1962 require constructor preconditions to be checked before or after the execution of the member initialization list?
Maybe the paper is not as clear as it could be, but the intend is *before* the member initializer list.
-Thorsten
OK. I will probably end up documenting member-init > pre > ... as a limitation of Boost.Contract because I do not think I will be able to implement pre > member-init > ... On Sun, Apr 11, 2010 at 10:58 AM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
From: "Lorenzo Caminiti" <lorcaminiti@gmail.com> CONSTRUCTORS Does n1962 require constructor preconditions to be checked before or after the execution of the member initialization list?
Hi Lorenzo, I supose that the constructor preconditions are evaluated before the member initialization as this initialization can rely on the preconditions been satisfied. Note also that preconditions/postconditions must to be in the declaration part, and the member initialization is on the definition part.
Indeed this is exactly why Boost.Contract has the limitation that when member initialization list is used, the constructor definition needs to appear together with the contract specification in the class declaration.
I understand that it is not easy for Boost.Contract to check the precondition before member initialization . To be able to do that you will need to have a first member or inherit from a 'precondition' class that do this precondition check,
class C : C_constructor_precondition ... {
C(T1 p1) : C_constructor_precondition(p1), ... { // ... } };
but this seems to me a severe constraint and adds more complexity. I think that I can live with preconditions check after member initialization.
Yes, this is also the _only_ option I could see to implement pre> member-init. I have experimented with it in the past and, as you indicate, it has significant problems: 1) I messes up with the inheritance tree (minor issue). 2) The precondition assertions are known where the constructor is specified but now they also need to be known by C_constructor_precondition -- how can this be done?? 3) Things get even more complex when considering multiple constructors with different arguments and different precondition assertions -- this will probably require to use different C_constructor_precondition_arg1, C_constructor_precondition_arg2, etc base classes -- but what would constructor(arg1) do with C_constructor_precondition_arg2?? 4) How do you wrap all of these within a single CONTRACT_CONSTRUCTOR() macro?? I have also experimented with using special member variables instead of base classes: class C: B { C(T1 p1): B(p1), c_p1_pre_(p1), ... { ... }; struct C_p1_pre_ { C_p1_pre_(T1 p1) { ASSERT(...); } } c_p1_pre_; ... }; But this way the preconditions are not checked before the base classes B(p1) are constructed which is not acceptable (plus how to I know if B(p1) is a same init or a member init so to inject c_p1_pre_(p1) in the right place?). (*) The advantage of this would be that struct can be defined by CONTRACT_CONSTRUCT() expansion. For multiple constructors, perhaps providing a default constructor to C_p1_pre_ that asserts nothing would allow other constructors not to worry about each others preconditions... However, I do not think (*) is acceptable so I stopped looking into this. I essentially gave up on trying to implement pre > member-init. While I now understand that member-init > pre is not ideal, I did not find this limitation relevant in practice when using Boost.Contract to program the examples and my ~60k lines of C++ project. (I wondered if delegating constructors could help, but I have not really looked into it.) Thanks, Lorenzo
On Sun, Apr 11, 2010 at 7:49 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
Agreed: the most constructive way to discuss policies 6) and 7) is for me to present examples. I will work on this.
I checked that the current Boost.Contract implementation follows the policies 6) and 7) as originally specified in n1613 (the original revision on n1962). I would like to ask for additional clarifications on the rational for changing (relaxing) these policies in subsequent revisions of the CP C++ standard proposal. On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy) n1962 only disables assertion checking from within preconditions checking. Instead, Boost.Contract disables assertion checking from within all contract checking.
I found this policy useful to prevent infinite recursion. Previous revisions of n1962 (n1613) specified the same policy implemented by Boost.Contract. Furthermore, Eiffel implements the Boost.Contract policy. Boost.Contract could be changed to comply with n1962.
Why does n1962 disable assertion checking only from within preconditions?
You got it the wrong way. Preconditions /never/ disable anything. You can prove that if you do so, an incorrect parameter might be passed on to the function body.
Revision history for 6) "disabling of checks during assertions": yes, but not in preconditions -- n1962 ** latest proposal revision ** no -- n1866, n1773 yes -- n1669, n1613 ** current Boost.Contract **
From n1613: <<There is one global rule about assertions and it is that assertions must be disabled in assertions. This removes the possibility of infinite recursion and allows a reasonable performance even with assertions enabled. With- out disabling assertions, infinite recursion will happen when a public func- tion appears in the invariant.>> This is also the policy that Eiffel follows.
Does n1962 policy introduce the opportunity for infinite recursion? For example: class x { CONTRACT_CLASS( (x) ) CONTRACT_FUNCTION( (bool) (g)( (int)(x) ) (const) (precondition) ( ( f(x) ) ) ({ return true; }) ) CONTRACT_FUNCTION( (bool) (f)( (int)(x) ) (const) (precondition) ( ( g(x) ) ) ({ return false; }) ) }; Call sequence without disabling assertions from preconditions: call x::f(x) -> check x::f(x) pre -> call x::g(x) -> check x::g(x) pre -> x::f(x) (infinite recursion) ... Call sequence disabling assertions when checking assertions (also for preconditions): call x::f(x) -> check x::f(x) pre -> call x::g(x) -> return true (x::g(x) precondition check is disabled, no infinite recursion) -> x::f(x) body ... On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
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?
Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function.
Revision history for 7) "when public func. call public func.": disable nothing -- n1962, n1886, n1773 ** latest proposal revision ** disable invariant -- n1669, n1613 ** current Boost.Contract **
From n1613: <<When calls to public member functions are nested, the invariant is not checked before and after the inner call. This is because the invariant is al- lowed to be temporarily broken within a call to a public function. The other contracts of the functions must still be checked though (see also section 7 on page 18).>> Eiffel disables all checks (invariants, preconditions, and postconditions).
(I incorrectly stated this will lead to infinite recursion but that is not the case based on 6). Therefore, I do not an infinite recursion example for this.) For both 6) and 7), note that it would be trivial to change Boost.Contract to fully comply with n1962. I am honestly trying to understand which policies are the best ones given that the different C++ proposal revisions and Eiffel all seem to use somewhat different specifications on this. Thank you very much for your help. Lorenzo
Lorenzo Caminiti skrev:
On Sun, Apr 11, 2010 at 7:49 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
Agreed: the most constructive way to discuss policies 6) and 7) is for me to present examples. I will work on this.
I checked that the current Boost.Contract implementation follows the policies 6) and 7) as originally specified in n1613 (the original revision on n1962). I would like to ask for additional clarifications on the rational for changing (relaxing) these policies in subsequent revisions of the CP C++ standard proposal.
Revision history for 6) "disabling of checks during assertions": yes, but not in preconditions -- n1962 ** latest proposal revision ** no -- n1866, n1773 yes -- n1669, n1613 ** current Boost.Contract **
From n1613: <<There is one global rule about assertions and it is that assertions must be disabled in assertions. This removes the possibility of infinite recursion and allows a reasonable performance even with assertions enabled. With- out disabling assertions, infinite recursion will happen when a public func- tion appears in the invariant.>> This is also the policy that Eiffel follows.
First of, the problem is not so big IMO. If your tests runs all functions, the infinite recursion is easy to detect and fix. D disables nothing, which we found somewhat silly since it is merely leading to poorer performance in debug-builds and adds cheks that are unlikely to recove any real errors (it deals mostly with "second hand errors"). Preconditions, OTOH, need to be checked to ensure correctness. -Thorsten
On Wed, Apr 14, 2010 at 4:50 PM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
Lorenzo Caminiti skrev:
On Sun, Apr 11, 2010 at 7:49 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
Agreed: the most constructive way to discuss policies 6) and 7) is for me to present examples. I will work on this.
I checked that the current Boost.Contract implementation follows the policies 6) and 7) as originally specified in n1613 (the original revision on n1962). I would like to ask for additional clarifications on the rational for changing (relaxing) these policies in subsequent revisions of the CP C++ standard proposal.
Revision history for 6) "disabling of checks during assertions": yes, but not in preconditions -- n1962 ** latest proposal revision ** no -- n1866, n1773 yes -- n1669, n1613 ** current Boost.Contract **
From n1613: <<There is one global rule about assertions and it is that
assertions must be disabled in assertions. This removes the possibility of infinite recursion and allows a reasonable performance even with assertions enabled. With- out disabling assertions, infinite recursion will happen when a public func- tion appears in the invariant.>> This is also the policy that Eiffel follows.
First of, the problem is not so big IMO. If your tests runs all functions, the infinite recursion is easy to detect and fix.
D disables nothing, which we found somewhat silly since it is merely leading to poorer performance in debug-builds and adds cheks that are unlikely to recove any real errors (it deals mostly with "second hand errors").
Preconditions, OTOH, need to be checked to ensure correctness.
I understand. Checking for correctness is the main objective of Boost.Contract so I will change the library to not disable any assertion checking in preconditions. Unless there are objections, I will also provide a configuration macro CONTRACT_CONFIG_DISABLE_ASSERTION_CHECKING_IN_PRECONDITION (default value 0) for programmers that are more concerned with the infinite recursion issue. Is there a code example of how CONTRACT_CONFIG_DISABLE_ASSERTION_CHECKING_IN_PRECONDITION=1 will brake correctness? I would like to add it to the library documentation.
On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto@cs.aau.dk> wrote:
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?
Because the callee does not know if the invariant has been proper established by the caller. The caller cares about the invariant on entrance/exit, but now must also do so when calling another public function.
I do not fully understand this... is there a code example?
Revision history for 7) "when public func. call public func.": disable nothing -- n1962, n1886, n1773 ** latest proposal revision ** disable invariant -- n1669, n1613 ** current Boost.Contract **
From n1613: <<When calls to public member functions are nested, the invariant is not checked before and after the inner call. This is because the invariant is al- lowed to be temporarily broken within a call to a public function. The other contracts of the functions must still be checked though (see also section 7 on page 18).>>
Is this still true? If yes, how does it reconcile with the issue above of the callee not knowing if the invariant has been established by the caller? Thank you very much. Lorenzo
vicente.botet wrote:
VBE> Boost.ScopeExit showed a technique that can be used to emulate local functions. Alexander proposed long time ago to provide it independently from ScopeExit but to my knowledge this has not been done.
Sorry for the late reply, I'm not following every boost thread, I got this message via google alerts. Yes, this has not been done. Local function can borrow argument binding syntax from ScopeExit but there are other things I need to think of. For instance, in int BOOST_LOCAL_FUNCTION(f, (BOOST_LOCAL_FUNCTION_BIND( (a)(&b) ), int c)) { // ... } BOOST_LOCAL_FUNCTION_END syntax, is there any way to shorten BOOST_LOCAL_FUNCTION_BIND to "bind"? The syntax doesn't have to be exactly as above. If someone could take a lead on this it would be great. I don't have time for this, I'm afraid. Alex
On Thu, Apr 15, 2010 at 7:02 PM, Alexander Nasonov <alnsn@yandex.ru> wrote:
vicente.botet wrote:
VBE> Boost.ScopeExit showed a technique that can be used to emulate local functions. Alexander proposed long time ago to provide it independently from ScopeExit but to my knowledge this has not been done.
Sorry for the late reply, I'm not following every boost thread, I got this message via google alerts.
No problem: There is no rush and thanks a lot for your reply.
Yes, this has not been done. Local function can borrow argument binding syntax from ScopeExit but there are other things I need to think of. For instance, in
int BOOST_LOCAL_FUNCTION(f, (BOOST_LOCAL_FUNCTION_BIND( (a)(&b) ), int c)) { // ... } BOOST_LOCAL_FUNCTION_END
syntax, is there any way to shorten BOOST_LOCAL_FUNCTION_BIND to "bind"?
For using this in Boost.Contract I see the following issues: 1) The CONTRACT_BLOCK_INVARIANT() macro will have to take as parameters also `a`, `&b`, `int`, `c`, etc. This is as complex as requesting the user to program a separate (private) member const function with these const parameters and then call that function to check the block invariant condition in a constant-correct context: struct x { void f(int a) { int b = a; // CONTRACT_BLOCK_INVARIANT(a == b); // Don't use this because it is not const-correct. CONTRACT_BLOCK_INVARIANT(equal(a, b)); // Const-correct. ... } private: bool equal(const int& a, cont int& b) const { return a == b; } // Const-correct for a, b, and object this. }; 2) How do I make the object (this) available within the local function? I could pass it as a 'self' parameter but then the assertion code will have to say, for example, `self.size()` instead of just `size()` and that is less readable...
The syntax doesn't have to be exactly as above. If someone could take a lead on this it would be great. I don't have time for this, I'm afraid.
I will experiment with this a bit more. If I can use BOOST_LOCAL_FUNCTION_... for CONTRACT_BLOCK_INVARIANT() (resolving issues 1) and 2) above) then I am happy to take the lead in separating this functionality from Boost.ScopeExit as part of Boost.Contract development. -- Lorenzo
participants (5)
-
Alexander Nasonov -
Lorenzo Caminiti -
Steven Watanabe -
Thorsten Ottosen -
vicente.botet