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 04:04:19

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_at_[hidden]>

> AMDG
>
> On 08/26/2012 05:36 PM, Lorenzo Caminiti wrote:
> > On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj_at_[hidden]>
> 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
>