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

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-08-27 15:25:29

On Mon, Aug 27, 2012 at 9:10 AM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
> 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.

No problem, it's always good to discuss :)

--Lorenzo