[contract] assertion requirements as meta-functions or not?

Hello all, Boost.Contract allows to specify "assertion requirements": /assertion-condition/, requires /assertion-requirement/ If the requirement is not met then the assertion condition is neither compiled nor checked at run-time. Question: Shall the assertion-requirement be a nullary boolean meta-function or just a static boolean value? For example: CONTRACT_FUNCTION( template( typename T ) requires( boost::LessThanComparable<T> ) (T const&) (min) ( (T const&) x, (T const&) y ) postcondition( auto result = return, x < y ? result == x : result == y, requires boost::has_equal_to<T>::value // static boolean ) ) { return x < y ? x : y; // OK: T is less than comparable `<`. } For now, the assertion requirement is a static boolean value so it can be more easily manipulated (using !, &&, ||, etc instead of mpl::not, mpl::and, mpl::or, etc). However, is there any strong reason for marking the assertion requirement a nullary boolean meta-function instead like the following code? x < y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function Thanks. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-assertion-requirements-as-... Sent from the Boost - Dev mailing list archive at Nabble.com.

Hi Lorenzo, If I understand your question and Boost.Contract design correctly, it looks like the former approach is more flexible in cases where I do _not_ want to use a meta-function to describe a constraint: postcondition( auto result = return, some_cond1(result), requires x / 2 == 0, some_cond2(result), requires noexcept(x), some_cond3(result), requires sizeof(x) > 2, ) Although I am not sure if such constraints would be useful in real life. Regards, &rzej. 2012/4/24 lcaminiti <lorcaminiti@gmail.com>
Hello all,
Boost.Contract allows to specify "assertion requirements":
/assertion-condition/, requires /assertion-requirement/
If the requirement is not met then the assertion condition is neither compiled nor checked at run-time.
Question: Shall the assertion-requirement be a nullary boolean meta-function or just a static boolean value?
For example:
CONTRACT_FUNCTION( template( typename T ) requires( boost::LessThanComparable<T> ) (T const&) (min) ( (T const&) x, (T const&) y ) postcondition( auto result = return, x < y ? result == x : result == y, requires boost::has_equal_to<T>::value // static boolean ) ) { return x < y ? x : y; // OK: T is less than comparable `<`. }
For now, the assertion requirement is a static boolean value so it can be more easily manipulated (using !, &&, ||, etc instead of mpl::not, mpl::and, mpl::or, etc). However, is there any strong reason for marking the assertion requirement a nullary boolean meta-function instead like the following code?
x < y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function
Thanks. --Lorenzo
-- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-assertion-requirements-as-... Sent from the Boost - Dev mailing list archive at Nabble.com.
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost

Andrzej Krzemienski wrote
Hi Lorenzo, If I understand your question and Boost.Contract design correctly, it looks like the former approach is more flexible in cases where I do _not_ want to use a meta-function to describe a constraint:
postcondition( auto result = return, some_cond1(result), requires x / 2 == 0, some_cond2(result), requires noexcept(x), some_cond3(result), requires sizeof(x) > 2, )
Yes, that is correct but I was wondering if there's any strong reason in favor of using a nullary boolean meta-function instead of sizeof(x) > 2, etc (I couldn't find such a reason myself and that's why I opted for the static boolean value).
Although I am not sure if such constraints would be useful in real life.
Assertions requirements are definitely useful for the basic has_equal_to<T> case (as you and I discussed a while back). Take the vector<T>::push_back example where T is not required to be EqualityComparable by the STL but it is if you program the postconditions and that can be modeled as: postcondition( back() == value, requires has_equal_to<T>::value ... ) Now you use the contracted vector class as usual and the postcondition is checked only when you use such a class on an EqualityComparable type T. Another interesting use of assertion requirements is to model computational complexity. Sometimes the contracts can be more expensive to check than the body itself :( so it is useful to disable specific assertions that might be too expensive (previous N1962 revisions used to do this introducing the notion of "importance ordering" then N1962 gave up on this feature -- assertion requirements are more general than importance ordering and they can be used also in this context). For example: #deifne O_1 0 #deifne O_N 1 ... postcondition( auto result = return, result == (find(begin(), end(), value) != end()), requires O_N <= COMPLEXITY_MAX ) If you compile this code with #define COMPLEXITY_MAX O_N (or greater) than this postcondition will be checked otherwise it will neither be compiled nor checked at run-time. So using assertion requirements you can program the notion "this assertion requires a computational complexity of O(n)" and then enable or disable all assertions with a complexity greater than some maximum set complexity COMPLEXITY_MAX. IMO, this might be useful too. (Of course, all this can be done just as well if assertion requirements are specified using a nullary boolean meta-functions but I saw no reason for that so I'm asking the ML.) Thanks. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-assertion-requirements-as-... Sent from the Boost - Dev mailing list archive at Nabble.com.

2012/4/24 lcaminiti <lorcaminiti@gmail.com>
Andrzej Krzemienski wrote
Hi Lorenzo, If I understand your question and Boost.Contract design correctly, it looks like the former approach is more flexible in cases where I do _not_ want to use a meta-function to describe a constraint:
postcondition( auto result = return, some_cond1(result), requires x / 2 == 0, some_cond2(result), requires noexcept(x), some_cond3(result), requires sizeof(x) > 2, )
Yes, that is correct but I was wondering if there's any strong reason in favor of using a nullary boolean meta-function instead of sizeof(x) > 2, etc (I couldn't find such a reason myself and that's why I opted for the static boolean value).
Although I am not sure if such constraints would be useful in real life.
Assertions requirements are definitely useful for the basic has_equal_to<T> case (as you and I discussed a while back). Take the vector<T>::push_back example where T is not required to be EqualityComparable by the STL but it is if you program the postconditions and that can be modeled as:
postcondition( back() == value, requires has_equal_to<T>::value ... )
Now you use the contracted vector class as usual and the postcondition is checked only when you use such a class on an EqualityComparable type T.
Sorry, I guess I was a bit imprecise. I did not want to suggest that conditional assertions were not useful (I agree with you that they are), but I was wondering if there is any useful condition that is not a meta-function. From your examples it looks like there is. I am not sure if the example where requirements EqualityComparable or CopyConstructible are stated is the most fortunate one -- someone may argue that Reularity is so essential tat a special case should be made for it anyway, similarly to function eq() in: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3351.pdf. This is why I like your other example with LessThanComparable better: https://svn.boost.org/svn/boost/sandbox/contract/libs/contract/doc/html/cont... Another interesting use of assertion requirements is to model computational
complexity. Sometimes the contracts can be more expensive to check than the body itself :( so it is useful to disable specific assertions that might be too expensive (previous N1962 revisions used to do this introducing the notion of "importance ordering" then N1962 gave up on this feature -- assertion requirements are more general than importance ordering and they can be used also in this context). For example:
#deifne O_1 0 #deifne O_N 1 ...
postcondition( auto result = return, result == (find(begin(), end(), value) != end()), requires O_N <= COMPLEXITY_MAX )
If you compile this code with #define COMPLEXITY_MAX O_N (or greater) than this postcondition will be checked otherwise it will neither be compiled nor checked at run-time.
So using assertion requirements you can program the notion "this assertion requires a computational complexity of O(n)" and then enable or disable all assertions with a complexity greater than some maximum set complexity COMPLEXITY_MAX. IMO, this might be useful too.
(Of course, all this can be done just as well if assertion requirements are specified using a nullary boolean meta-functions but I saw no reason for that so I'm asking the ML.)
This is a nice example. I would also add that there are some assertions that can be expressed but must never be evaluated because they would alter the behavior of the function, like iterating over an input range. Regards, &rzej

Le 24/04/12 14:31, lcaminiti a écrit :
Hello all,
Boost.Contract allows to specify "assertion requirements":
/assertion-condition/, requires /assertion-requirement/
If the requirement is not met then the assertion condition is neither compiled nor checked at run-time.
Question: Shall the assertion-requirement be a nullary boolean meta-function or just a static boolean value?
For example:
CONTRACT_FUNCTION( template( typename T ) requires( boost::LessThanComparable<T> ) (T const&) (min) ( (T const&) x, (T const&) y ) postcondition( auto result = return, x< y ? result == x : result == y, requires boost::has_equal_to<T>::value // static boolean ) ) { return x< y ? x : y; // OK: T is less than comparable `<`. }
For now, the assertion requirement is a static boolean value so it can be more easily manipulated (using !,&&, ||, etc instead of mpl::not, mpl::and, mpl::or, etc). However, is there any strong reason for marking the assertion requirement a nullary boolean meta-function instead like the following code?
x< y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function
Hi, I don't know if following the the _c suffix rule in Boost could help. x< y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function and x< y ? result == x : result == y, requires*_c* boost::has_equal_to<T>::value // value Best, Vicente

Vicente Botet wrote
Le 24/04/12 14:31, lcaminiti a écrit :
Hello all,
Boost.Contract allows to specify "assertion requirements":
/assertion-condition/, requires /assertion-requirement/
If the requirement is not met then the assertion condition is neither compiled nor checked at run-time.
Question: Shall the assertion-requirement be a nullary boolean meta-function or just a static boolean value?
For example:
CONTRACT_FUNCTION( template( typename T ) requires( boost::LessThanComparable<T> ) (T const&) (min) ( (T const&) x, (T const&) y ) postcondition( auto result = return, x< y ? result == x : result == y, requires boost::has_equal_to<T>::value // static boolean ) ) { return x< y ? x : y; // OK: T is less than comparable `<`. }
For now, the assertion requirement is a static boolean value so it can be more easily manipulated (using !,&&, ||, etc instead of mpl::not, mpl::and, mpl::or, etc). However, is there any strong reason for marking the assertion requirement a nullary boolean meta-function instead like the following code?
x< y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function
Hi,
I don't know if following the the _c suffix rule in Boost could help.
x< y ? result == x : result == y, requires boost::has_equal_to<T> // meta-function
and
x< y ? result == x : result == y, requires*_c* boost::has_equal_to<T>::value // value
Yes, that is possible and a reasonable suggestion but I fear it will be confusing for the user. There are already a lot of syntactic elements users need to familiarize themselves in using Boost.Contract so I'd rather pick one syntax (meta-function or not) and offer just that. Users can make meta-functions from static values and vice versa if they need to. Thanks. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-assertion-requirements-as-... Sent from the Boost - Dev mailing list archive at Nabble.com.
participants (3)
-
Andrzej Krzemienski
-
lcaminiti
-
Vicente J. Botet Escriba