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

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-08-27 07:42:15

2012/8/27 Andrzej Krzemienski <akrzemi1_at_[hidden]>

> The bug it has is that on some situations it fails to satisfy the
> postcondition. It incorrectly uses the tool for avoiding postcondition
> violations (i.e., exception handling mechanism). Boost.Contract library has
> enough power to be able to detect this bug; provided it follows the rule
> "function postconditions must be satisfied even if the function exits via
> an exception."
>
> Now, I hear that this is not what N1962 or Eiffel do. But to me it only
> means that both N1962 and Eiffel got it wrong. I realize that what I say is
> daring. But then again this is where I see the value of Boost.Contract
> library: It can verify in practise if N1962 makes sense, and how it can be
> improved.
>

I have just found that two years ago when Lorenzo introduced his Contract
library I was expecting just the opposite behavior (the current behavior of
the library):
https://groups.google.com/d/msg/boost-developers-archive/7fEtk3Gdgh0/Dl3lYeraMoUJ

But still, as of today, checking postconditions on throw appears to me to
be a better approach.

Regards,
&rzej