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

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