
26 Aug
2012
26 Aug
'12
10:32 p.m.
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. In Christ, Steven Watanabe