Subject: Re: [boost] [contract] Broken postconditions on throw
From: Steven Watanabe (watanabesj_at_[hidden])
Date: 2012-08-26 20:51:33
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