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