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

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-08-26 20:36:11

On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj_at_[hidden]> 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