Re: [boost] [contract] Broken postconditions on throw

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-08-27 12:10:42

2012/8/27 Andrzej Krzemienski <akrzemi1_at_[hidden]>

> 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