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:
> On 08/26/2012 12:10 PM, Andrzej Krzemienski wrote:
>> 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
> This doesn't violate the postcondition.
> postconditions are only valid if the function
> returns normally.
This is correct -- see for example note  of N1962:
 Note that if an exception is thrown in the function body, the
postcondition is not evaluated.
But also Eiffel (and probably D).
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk