On Sun, Aug 26, 2012 at 3:32 PM, Steven Watanabe <watanabesj@gmail.com> 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