[contract] Broken postconditions on throw
Hi Lorenzo, I am now now playing with Contract library and trying to break it. I checked that the framework checks the class invariant even when member function exits via an exception. This is an expected behavior and the framework is working fine. However, I note that the precondition of a (non-member) function is not checked when the function exits via throwing an exception. See the following program: # include <contract.hpp> double get_random_weight() { return -1.0; // erroneous implementation } CONTRACT_FUNCTION ( void (set_weight)( (double&) w ) postcondition(w >= 0.0) ) { w = get_random_weight(); if (w < 0.0) throw 1; // (*) } int main() try { double w = 0.0; set_weight(w); } catch (...) { std::cerr << "CAUGHT EXCEPTION" << std::endl; } Function set_weight() is intended to assign its (output) argument with a value representing weight (in the physical sense). We guarantee that the value we set is always non-negative. The function clumsily attempts to verify the condition itself (the line with *). It signals the failure with an exception, but unfortunately fails to satisfy the postcondition. I expect that this situation should be reported as a postcondition violation. But no violation is reported, and the program successfully outputs "CAUGHT EXCEPTION". Regards, &rzej
AMDG On 08/26/2012 12:10 PM, Andrzej Krzemienski wrote:
<snip> Function set_weight() is intended to assign its (output) argument with a value representing weight (in the physical sense). We guarantee that the value we set is always non-negative. The function clumsily attempts to verify the condition itself (the line with *). It signals the failure with an exception, but unfortunately fails to satisfy the postcondition. I expect that this situation should be reported as a postcondition violation. But no violation is reported, and the program successfully outputs "CAUGHT EXCEPTION".
This doesn't violate the postcondition. postconditions are only valid if the function returns normally. In Christ, Steven Watanabe
On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj@gmail.com> wrote:
AMDG
On 08/26/2012 12:10 PM, Andrzej Krzemienski wrote:
<snip> Function set_weight() is intended to assign its (output) argument with a value representing weight (in the physical sense). We guarantee that the value we set is always non-negative. The function clumsily attempts to verify the condition itself (the line with *). It signals the failure with an exception, but unfortunately fails to satisfy the postcondition. I expect that this situation should be reported as a postcondition violation. But no violation is reported, and the program successfully outputs "CAUGHT EXCEPTION".
This doesn't violate the postcondition. postconditions are only valid if the function returns normally.
This is correct -- see for example note [11] of N1962: [11] Note that if an exception is thrown in the function body, the postcondition is not evaluated. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html#id46 But also Eiffel (and probably D). --Lorenzo
AMDG On 08/26/2012 05:36 PM, Lorenzo Caminiti wrote:
On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj@gmail.com> wrote:
This doesn't violate the postcondition. postconditions are only valid if the function returns normally.
This is correct -- see for example note [11] of N1962:
[11] Note that if an exception is thrown in the function body, the postcondition is not evaluated.
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html#id46
But also Eiffel (and probably D).
Anything else doesn't even make sense. If you can satisfy the postconditions, there's no reason to throw an exception in the first place. In Christ, Steven Watanabe
Steven, Lorenzo, Either I do not understand what you are saying you or you do not understand what I am saying. Let me try to explain my reasoning. Sorry if I say too obvious thing but I want to make sure I am understood. First, function set_weight() I described above is obviously wrong (intentionally). I am testing a library whose purpose is to detect bugs in the code. So I am testing it by writing buggy code and checking if the library finds all the bugs (that it is supposed to find). The correct way of writing my function would be (I am using an ideal syntax): void set_weight( double& w ) postcondition(w >= 0.0) { double tmp = get_random_weight(); if (tmp < 0.0) throw 1; w = wgt; } Note the following. If the function observes that it would not be able to satisfy the postcondition then and only then does it decide to throw an exception. Or in other words: it throws an exception in order not to violate the postcondition. It follows the rule expressed by Dave Abrahams recently (see here: http://cpp-next.com/archive/2012/08/evil-or-just-misunderstood/#comment-2036): "Exceptions are (in general) for avoiding postcondition failure." Now, if you look at my faulty implementation of set_weight again: void set_weight( double& w ) postcondition(w >= 0.0) { w = get_random_weight(); if (w < 0.0) throw 1; } The bug it has is that on some situations it fails to satisfy the postcondition. It incorrectly uses the tool for avoiding postcondition violations (i.e., exception handling mechanism). Boost.Contract library has enough power to be able to detect this bug; provided it follows the rule "function postconditions must be satisfied even if the function exits via an exception." Now, I hear that this is not what N1962 or Eiffel do. But to me it only means that both N1962 and Eiffel got it wrong. I realize that what I say is daring. But then again this is where I see the value of Boost.Contract library: It can verify in practise if N1962 makes sense, and how it can be improved. If the goal of the library is to implement what N1962 proposes, then you already showed that it does. But if the goal is to get the contracts right, then it is still worth reconsidering how the postcondition violation on throw should be handled. If you feel N1962 got it right, then I propose adding a rationale for it, because, as you can see, I am unconvinced; and I expect that others may also find this behavior surprising. Regards, &rzej 2012/8/27 Steven Watanabe <watanabesj@gmail.com>
AMDG
On 08/26/2012 05:36 PM, Lorenzo Caminiti wrote:
On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj@gmail.com> wrote:
This doesn't violate the postcondition. postconditions are only valid if the function returns normally.
This is correct -- see for example note [11] of N1962:
[11] Note that if an exception is thrown in the function body, the postcondition is not evaluated.
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html#id46
But also Eiffel (and probably D).
Anything else doesn't even make sense. If you can satisfy the postconditions, there's no reason to throw an exception in the first place.
In Christ, Steven Watanabe
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
2012/8/27 Andrzej Krzemienski <akrzemi1@gmail.com>
The bug it has is that on some situations it fails to satisfy the postcondition. It incorrectly uses the tool for avoiding postcondition violations (i.e., exception handling mechanism). Boost.Contract library has enough power to be able to detect this bug; provided it follows the rule "function postconditions must be satisfied even if the function exits via an exception."
Now, I hear that this is not what N1962 or Eiffel do. But to me it only means that both N1962 and Eiffel got it wrong. I realize that what I say is daring. But then again this is where I see the value of Boost.Contract library: It can verify in practise if N1962 makes sense, and how it can be improved.
I have just found that two years ago when Lorenzo introduced his Contract library I was expecting just the opposite behavior (the current behavior of the library): https://groups.google.com/d/msg/boost-developers-archive/7fEtk3Gdgh0/Dl3lYer... But still, as of today, checking postconditions on throw appears to me to be a better approach. Regards, &rzej
Le 27/08/12 13:42, Andrzej Krzemienski a écrit :
2012/8/27 Andrzej Krzemienski <akrzemi1@gmail.com>
I have just found that two years ago when Lorenzo introduced his Contract library I was expecting just the opposite behavior (the current behavior of the library): https://groups.google.com/d/msg/boost-developers-archive/7fEtk3Gdgh0/Dl3lYer...
There is a point in this thread I would like to discuss. " (7) The documentation lists the following sequence for executing a constructor: 1. Initialize member variables via the constructor member initialization list (if such a list is specified). 2. Check preconditions (but not invariants). 3. Execute constructor body. 4. Check invariants. 5. Check postconditions. I believe, one of the reasons for validating arguments of a constuctor is to not allow the incorrect values to initialize objest's sub-objects (members). I believe the sequence of the first two items should be inverse. Am I wrong? " I think both of you agree that providing the sequence {Pre AND Initializers} will be better than {Initializers AND Pre}, but we don't know yet how to implement it. I have not seen yet the code generated by the macros, but one technique that maybe could be used is to add a dummy field that will be the first of the class. This parameter will be generated by the CONTRACT_CLASS macro and initialized by the generated function evaluating the preconditions. CONTRACT_CONSTRUCTOR( // Declare the constructor and its contract. public explicit (ivector) ( (size_type) count ) precondition( count >= 0 ) postcondition( size() == count, boost::algorithm::all_of_equal(begin(), end(), 0) ) initialize( vector_(count) ) ) {} dummy_type precondition1(size_type count) { if (count >= 0 ) return dummy_type(); else invalidate_contract(); } ivector(size_type count) : dummy(precondition1(count), vector_(count) { // body // post condition check // class invariant check } Of course, this has the liability to add an extra field. The other drawback is that initializer should be split in two parts the base class initializers and the field initializers. Best, Vicente
On Tue, Aug 28, 2012 at 10:04 AM, Vicente J. Botet Escriba <vicente.botet@wanadoo.fr> wrote:
Le 27/08/12 13:42, Andrzej Krzemienski a écrit :
2012/8/27 Andrzej Krzemienski <akrzemi1@gmail.com>
I have just found that two years ago when Lorenzo introduced his Contract library I was expecting just the opposite behavior (the current behavior of the library): https://groups.google.com/d/msg/boost-developers-archive/7fEtk3Gdgh0/Dl3lYer...
There is a point in this thread I would like to discuss.
" (7)
The documentation lists the following sequence for executing a constructor:
1. Initialize member variables via the constructor member initialization list (if such a list is specified). 2. Check preconditions (but not invariants). 3. Execute constructor body. 4. Check invariants. 5. Check postconditions.
Where do the docs say the above? That's incorrect... In the Contract Programming Overview section, the docs say: http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_... `` A constructor call executes the following steps: 1. Check the constructor preconditions. 2. Initialize base classes and members executing the constructor member initialization list if present. 3. Check the static class invariants (but not the non-static class invariants). 4. Execute the constructor body. 5. Check the static class invariants (even if the body throws an exception). 6. Check the non-static class invariants, but only if the body did not throw an exception. 7. Check the constructor postconditions, but only if the body did not throw an exception. Preconditions are checked before initializing base classes and members so that these initializations can relay on preconditions to be true (for example to validate constructor arguments before they are used to initialize member variables). C++ object construction mechanism will automatically check base class contracts when subcontracting. '' Preconditions are checked before initializers (but static class invariants are not). That's in the spirit of N1962 (even if not explicitly stated as clarified by Thorsten a couple of years back in this ML, we all discussed this together). It wasn't at all easy to implement this... but it should work correctly now :D (essentially, I use and extra base class that is initlialized before anything else, pass it the pointer to the static member function that checks preconditions, and the base class constructor calls the function so it checks the pre).
I believe, one of the reasons for validating arguments of a constuctor is to not allow the incorrect values to initialize objest's sub-objects (members). I believe the sequence of the first two items should be inverse. Am I wrong? "
I think both of you agree that providing the sequence {Pre AND Initializers} will be better than {Initializers AND Pre}, but we don't know yet how to implement it.
I have not seen yet the code generated by the macros, but one technique that maybe could be used is to add a dummy field that will be the first of the class. This parameter will be generated by the CONTRACT_CLASS macro and initialized by the generated function evaluating the preconditions.
CONTRACT_CONSTRUCTOR( // Declare the constructor and its contract. public explicit (ivector) ( (size_type) count ) precondition( count >= 0 ) postcondition( size() == count, boost::algorithm::all_of_equal(begin(), end(), 0) ) initialize( vector_(count) ) ) {}
dummy_type precondition1(size_type count) { if (count >= 0 ) return dummy_type(); else invalidate_contract(); }
ivector(size_type count)
: dummy(precondition1(count),
vector_(count) {
// body
// post condition check
// class invariant check }
Of course, this has the liability to add an extra field.
The other drawback is that initializer should be split in two parts the base class initializers and the field initializers.
Thanks, --Lorenzo
2012/8/28 Lorenzo Caminiti <lorcaminiti@gmail.com>
" (7)
The documentation lists the following sequence for executing a constructor:
1. Initialize member variables via the constructor member initialization list (if such a list is specified). 2. Check preconditions (but not invariants). 3. Execute constructor body. 4. Check invariants. 5. Check postconditions.
Where do the docs say the above? That's incorrect...
Vicente quotes the thread from this list from two years ago. But the library has been changed since and executes the expected sequence of checks (preconditions first, initialization second). I already managed to test that :)
On Aug 28, 2012 11:43 AM, "Andrzej Krzemienski" <akrzemi1@gmail.com> wrote:
2012/8/28 Lorenzo Caminiti <lorcaminiti@gmail.com>
" (7)
The documentation lists the following sequence for executing a constructor:
1. Initialize member variables via the constructor member initialization list (if such a list is specified). 2. Check preconditions (but not invariants). 3. Execute constructor body. 4. Check invariants. 5. Check postconditions.
Where do the docs say the above? That's incorrect...
Vicente quotes the thread from this list from two years ago. But the library has been changed since and executes the expected sequence of
checks
(preconditions first, initialization second). I already managed to test that :)
BTW, to simply test contract execution printf-style, you can print in the assertions: precondition( std::clog << ... ) Because the output operator returns a stream that converts to bool true if no error, so a stream can be used in an assertion and to print if you are in a given pre/post/inv. HTH, --Lorenzo
2012/8/27 Andrzej Krzemienski <akrzemi1@gmail.com>
Steven, Lorenzo, Either I do not understand what you are saying you or you do not understand what I am saying. Let me try to explain my reasoning. Sorry if I say too obvious thing but I want to make sure I am understood.
First, function set_weight() I described above is obviously wrong (intentionally). I am testing a library whose purpose is to detect bugs in the code. So I am testing it by writing buggy code and checking if the library finds all the bugs (that it is supposed to find).
The correct way of writing my function would be (I am using an ideal syntax):
void set_weight( double& w ) postcondition(w >= 0.0) { double tmp = get_random_weight(); if (tmp < 0.0) throw 1; w = wgt; }
Note the following. If the function observes that it would not be able to satisfy the postcondition then and only then does it decide to throw an exception. Or in other words: it throws an exception in order not to violate the postcondition. It follows the rule expressed by Dave Abrahams recently (see here: http://cpp-next.com/archive/2012/08/evil-or-just-misunderstood/#comment-2036): "Exceptions are (in general) for avoiding postcondition failure."
Now, if you look at my faulty implementation of set_weight again:
void set_weight( double& w ) postcondition(w >= 0.0)
{ w = get_random_weight(); if (w < 0.0) throw 1; }
The bug it has is that on some situations it fails to satisfy the postcondition. It incorrectly uses the tool for avoiding postcondition violations (i.e., exception handling mechanism). Boost.Contract library has enough power to be able to detect this bug; provided it follows the rule "function postconditions must be satisfied even if the function exits via an exception."
Now, I hear that this is not what N1962 or Eiffel do. But to me it only means that both N1962 and Eiffel got it wrong. I realize that what I say is daring. But then again this is where I see the value of Boost.Contract library: It can verify in practise if N1962 makes sense, and how it can be improved.
If the goal of the library is to implement what N1962 proposes, then you already showed that it does. But if the goal is to get the contracts right, then it is still worth reconsidering how the postcondition violation on throw should be handled. If you feel N1962 got it right, then I propose adding a rationale for it, because, as you can see, I am unconvinced; and I expect that others may also find this behavior surprising.
Regards, &rzej
Oops. It looks like I have written some big nonsense. Obviously, if a function throws an exception to signal that it was not able to satisfy the postcondition, there is no point in still checking if it satisfied the postcondition -- we already know it didn't. The predicate I stated: (w >= 0.0) is not a postcondition bus some sort of "invariant on external state". There is nothing wrong with Boost.Concept or N1962 or Eiffel -- only with my head. It looks I still need to learn DbC. Sorry for this confusion. Regards, &rzej
On Mon, Aug 27, 2012 at 9:10 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2012/8/27 Andrzej Krzemienski <akrzemi1@gmail.com>
Steven, Lorenzo, Either I do not understand what you are saying you or you do not understand what I am saying. Let me try to explain my reasoning. Sorry if I say too obvious thing but I want to make sure I am understood.
First, function set_weight() I described above is obviously wrong (intentionally). I am testing a library whose purpose is to detect bugs in the code. So I am testing it by writing buggy code and checking if the library finds all the bugs (that it is supposed to find).
The correct way of writing my function would be (I am using an ideal syntax):
void set_weight( double& w ) postcondition(w >= 0.0) { double tmp = get_random_weight(); if (tmp < 0.0) throw 1; w = wgt; }
Note the following. If the function observes that it would not be able to satisfy the postcondition then and only then does it decide to throw an exception. Or in other words: it throws an exception in order not to violate the postcondition. It follows the rule expressed by Dave Abrahams recently (see here: http://cpp-next.com/archive/2012/08/evil-or-just-misunderstood/#comment-2036): "Exceptions are (in general) for avoiding postcondition failure."
Now, if you look at my faulty implementation of set_weight again:
void set_weight( double& w ) postcondition(w >= 0.0)
{ w = get_random_weight(); if (w < 0.0) throw 1; }
The bug it has is that on some situations it fails to satisfy the postcondition. It incorrectly uses the tool for avoiding postcondition violations (i.e., exception handling mechanism). Boost.Contract library has enough power to be able to detect this bug; provided it follows the rule "function postconditions must be satisfied even if the function exits via an exception."
Now, I hear that this is not what N1962 or Eiffel do. But to me it only means that both N1962 and Eiffel got it wrong. I realize that what I say is daring. But then again this is where I see the value of Boost.Contract library: It can verify in practise if N1962 makes sense, and how it can be improved.
If the goal of the library is to implement what N1962 proposes, then you already showed that it does. But if the goal is to get the contracts right, then it is still worth reconsidering how the postcondition violation on throw should be handled. If you feel N1962 got it right, then I propose adding a rationale for it, because, as you can see, I am unconvinced; and I expect that others may also find this behavior surprising.
Regards, &rzej
Oops. It looks like I have written some big nonsense. Obviously, if a function throws an exception to signal that it was not able to satisfy the postcondition, there is no point in still checking if it satisfied the postcondition -- we already know it didn't. The predicate I stated: (w >= 0.0) is not a postcondition bus some sort of "invariant on external state". There is nothing wrong with Boost.Concept or N1962 or Eiffel -- only with my head. It looks I still need to learn DbC.
No problem, it's always good to discuss :) --Lorenzo
participants (4)
-
Andrzej Krzemienski -
Lorenzo Caminiti -
Steven Watanabe -
Vicente J. Botet Escriba