[boost] [contract] oldof failure not in N1962?

classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

[boost] [contract] oldof failure not in N1962?

lcaminiti
Hello all (and especially N1962 authors),

As far as I can see, N1962 does not say what to do in case of a failure while evaluating and copying an oldof expression. For example, what shall Contract Programming do if there is a memory error while taking a copy of size() to later check the following postcondition?

    size() == oldof size() + 1

Given that oldof copies are taken just after preconditions are checked and before the body is executed, I am tempted to treat the oldof failure as a precondition failure and call the precondition_broken handler. An alternative would be to to treat the oldof failure as if it happened within the body. However, in this case the body will raise more errors (e.g., throw more exceptions) that it will raise without the oldof contracts so I don't think this is a good approach.

In summary:
1) oldof expressions belong to the contract therefore I think oldof failures should result in calling one of the contract failure handlers (precondition_broken or postcondition_broken).
2) Given that eventual oldof failures happen before the body is executed (and just after the preconditions are checked), I think precondition_broken should be called (instead of postcondition_broken) in case of an oldof failure.

The counter argument is that precondition failures indicate a bug in the caller. However, oldof failures indicate a system-level exception in the code that programs the program-- oldof failures are not bugs in neither the caller (precondition_broken) nor in the body implementation (postcondition_broken)... but if you follow this argument, you need to give up 1)...

What do you think?

Thank you.
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [boost] [contract] oldof failure not in N1962?

lcaminiti
lcaminiti wrote
Hello all (and especially N1962 authors),

As far as I can see, N1962 does not say what to do in case of a failure while evaluating and copying an oldof expression. For example, what shall Contract Programming do if there is a memory error while taking a copy of size() to later check the following postcondition?

    size() == oldof size() + 1

Given that oldof copies are taken just after preconditions are checked and before the body is executed, I am tempted to treat the oldof failure as a precondition failure and call the precondition_broken handler. An alternative would be to to treat the oldof failure as if it happened within the body. However, in this case the body will raise more errors (e.g., throw more exceptions) that it will raise without the oldof contracts so I don't think this is a good approach.

In summary:
1) oldof expressions belong to the contract therefore I think oldof failures should result in calling one of the contract failure handlers (precondition_broken or postcondition_broken).
2) Given that eventual oldof failures happen before the body is executed (and just after the preconditions are checked), I think precondition_broken should be called (instead of postcondition_broken) in case of an oldof failure.

The counter argument is that precondition failures indicate a bug in the caller. However, oldof failures indicate a system-level exception in the code that programs the program-- oldof failures are not bugs in neither the caller (precondition_broken) nor in the body implementation (postcondition_broken)... but if you follow this argument, you need to give up 1)...
I started implementing this in Boost.Contract and I realized that it might be better to call postcondition_broken but only after executing the body in case of an oldof failure. This is because the contract states that the body can be executed if the preconditions pass and that is the case even when oldof fail just before executing the body so the body should be executed anyway. Furthermore, an oldof failure does not allow to check the postcondition and given that we cannot assume the postconditions pass unless we check them, an oldof failure implies that the postconditions did not pass (because we could not check them at all).

For example, for a member function call, the contract checking pseudo-code will look like this:

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(!check_preconditions()) precondition_broken();
    bool oldof_failed = !copy_oldofs(); // keep going even if oldof failure

    try { body(); } // execute body
    catch(...) {
        if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
        throw;
    }

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(oldof_failed || !check_postconditions()) postcondition_broken();

Note how even in case of an oldof failure, the body is executed and the class invariants are checked on exit. Only after that, the eventual oldof failure is reported using postcondition_broken.

I'm thinking this the way to handle oldof failures that better match the contract definitions:
1) Body can be executed if invariants and preconditions pass.
2) Invariants on exit are checked if body pass and also if body throws.
3) Any contract condition fails if it cannot be checked (and postconditions cannot be checked if oldof cannot be copied).

--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [boost] [contract] oldof failure not in N1962?

Vicente Botet
lcaminiti wrote
lcaminiti wrote
Hello all (and especially N1962 authors),

As far as I can see, N1962 does not say what to do in case of a failure while evaluating and copying an oldof expression. For example, what shall Contract Programming do if there is a memory error while taking a copy of size() to later check the following postcondition?

    size() == oldof size() + 1

Given that oldof copies are taken just after preconditions are checked and before the body is executed, I am tempted to treat the oldof failure as a precondition failure and call the precondition_broken handler. An alternative would be to to treat the oldof failure as if it happened within the body. However, in this case the body will raise more errors (e.g., throw more exceptions) that it will raise without the oldof contracts so I don't think this is a good approach.

In summary:
1) oldof expressions belong to the contract therefore I think oldof failures should result in calling one of the contract failure handlers (precondition_broken or postcondition_broken).
2) Given that eventual oldof failures happen before the body is executed (and just after the preconditions are checked), I think precondition_broken should be called (instead of postcondition_broken) in case of an oldof failure.

The counter argument is that precondition failures indicate a bug in the caller. However, oldof failures indicate a system-level exception in the code that programs the program-- oldof failures are not bugs in neither the caller (precondition_broken) nor in the body implementation (postcondition_broken)... but if you follow this argument, you need to give up 1)...
I started implementing this in Boost.Contract and I realized that it might be better to call postcondition_broken but only after executing the body in case of an oldof failure. This is because the contract states that the body can be executed if the preconditions pass and that is the case even when oldof fail just before executing the body so the body should be executed anyway. Furthermore, an oldof failure does not allow to check the postcondition and given that we cannot assume the postconditions pass unless we check them, an oldof failure implies that the postconditions did not pass (because we could not check them at all).

For example, for a member function call, the contract checking pseudo-code will look like this:

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(!check_preconditions()) precondition_broken();
    bool oldof_failed = !copy_oldofs(); // keep going even if oldof failure

    try { body(); } // execute body
    catch(...) {
        if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
        throw;
    }

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(oldof_failed || !check_postconditions()) postcondition_broken();

Note how even in case of an oldof failure, the body is executed and the class invariants are checked on exit. Only after that, the eventual oldof failure is reported using postcondition_broken.

I'm thinking this the way to handle oldof failures that better match the contract definitions:
1) Body can be executed if invariants and preconditions pass.
2) Invariants on exit are checked if body pass and also if body throws.
3) Any contract condition fails if it cannot be checked (and postconditions cannot be checked if oldof cannot be copied).
Hi Lorenzo,

I don't remember what N1962 says, but I would force that preconditions and post conditions evaluation shall not throw. If an exception is throw during precondition evaluation, post-condition preparation or evaluation I would say the program should terminate, as the program can not state if the conditions are satisfied or not.

The users can always associate a handler to terminate.

Just my 2cts,
Vicente
Reply | Threaded
Open this post in threaded view
|

Re: [boost] [contract] oldof failure not in N1962?

lcaminiti
Vicente Botet wrote
lcaminiti wrote
lcaminiti wrote
Hello all (and especially N1962 authors),

As far as I can see, N1962 does not say what to do in case of a failure while evaluating and copying an oldof expression. For example, what shall Contract Programming do if there is a memory error while taking a copy of size() to later check the following postcondition?

    size() == oldof size() + 1

Given that oldof copies are taken just after preconditions are checked and before the body is executed, I am tempted to treat the oldof failure as a precondition failure and call the precondition_broken handler. An alternative would be to to treat the oldof failure as if it happened within the body. However, in this case the body will raise more errors (e.g., throw more exceptions) that it will raise without the oldof contracts so I don't think this is a good approach.

In summary:
1) oldof expressions belong to the contract therefore I think oldof failures should result in calling one of the contract failure handlers (precondition_broken or postcondition_broken).
2) Given that eventual oldof failures happen before the body is executed (and just after the preconditions are checked), I think precondition_broken should be called (instead of postcondition_broken) in case of an oldof failure.

The counter argument is that precondition failures indicate a bug in the caller. However, oldof failures indicate a system-level exception in the code that programs the program-- oldof failures are not bugs in neither the caller (precondition_broken) nor in the body implementation (postcondition_broken)... but if you follow this argument, you need to give up 1)...
I started implementing this in Boost.Contract and I realized that it might be better to call postcondition_broken but only after executing the body in case of an oldof failure. This is because the contract states that the body can be executed if the preconditions pass and that is the case even when oldof fail just before executing the body so the body should be executed anyway. Furthermore, an oldof failure does not allow to check the postcondition and given that we cannot assume the postconditions pass unless we check them, an oldof failure implies that the postconditions did not pass (because we could not check them at all).

For example, for a member function call, the contract checking pseudo-code will look like this:

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(!check_preconditions()) precondition_broken();
    bool oldof_failed = !copy_oldofs(); // keep going even if oldof failure

    try { body(); } // execute body
    catch(...) {
        if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
        throw;
    }

    if(!check_static_class_invariants() || !check_class_invariants()) class_invariant_broken();
    if(oldof_failed || !check_postconditions()) postcondition_broken();

Note how even in case of an oldof failure, the body is executed and the class invariants are checked on exit. Only after that, the eventual oldof failure is reported using postcondition_broken.

I'm thinking this the way to handle oldof failures that better match the contract definitions:
1) Body can be executed if invariants and preconditions pass.
2) Invariants on exit are checked if body pass and also if body throws.
3) Any contract condition fails if it cannot be checked (and postconditions cannot be checked if oldof cannot be copied).
Hi Lorenzo,

I don't remember what N1962 says, but I would force that preconditions and post conditions evaluation shall not throw. If an exception is throw during precondition evaluation, post-condition preparation or evaluation I would say the program should terminate, as the program can not state if the conditions are satisfied or not.

The users can always associate a handler to terminate.
Yes, that is how Boost.Contract works (same as N1962). If preconditions, postconditions, invariants, etc fail, handlers are called precondition/postcondition/class_invariant/block_invariant/loop_variant/broken_handler. These handlers call std::terminate by default but programmers can redefine them (e.g., set_precondition_broken) to do something else. Plus there is a context parameter to the handlers so you know if the contract failure came from a free function, a destructor, etc so you can avoid to throw from destructors even if you want to redefine the contract broken handlers to throw instead of terminating.

However, my question is about what shall it happen if an exception is raised while I am copying oldof values.

In general, if an exception is raised while evaluating preconditions, postconditions, and invariants the relative handler is called (pre/post/inv_broken). But there is not an handler for oldof failures (and I'd find it confusing to add one). So my last idea is that I call the postcondition_broken handler if an exception is thrown while copying oldof but only after I have executed also the body and checked the class invariants on exit. This is a bit of a technicality (not clarified by neither N1962, Eiffel, D, A++, etc as far as I can tell) but I think I got it right.

Thanks a lot.
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

Dave Abrahams
In reply to this post by Vicente Botet

on Mon Jul 18 2011, Vicente Botet <vicente.botet-AT-wanadoo.fr> wrote:

>
> Hi Lorenzo,
>
> I don't remember what N1962 says, but I would force that preconditions and
> post conditions evaluation shall not throw. If an exception is throw during
> precondition evaluation, post-condition preparation or evaluation I would
> say the program should terminate, as the program can not state if the
> conditions are satisfied or not.

That doesn't make any sense to me.  If you run out of memory while
evaluating a precondition, it means you can't evaluate the precondition,
not that the program can't recover.

My guidelines are:

- Use exceptions for recoverable conditions.

- Do not use exceptions for non-recoverable conditions

- Failure to satisfy a precondition is a program bug

- Program bugs are non-recoverable

- Anticipated failure to satisfy a postcondition (e.g. I can't get
  enough memory to do my job) is a recoverable condition

- An actual postcondition violations is a program bug.

HTH,

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

lcaminiti
On Tue, Jul 19, 2011 at 10:48 AM, Dave Abrahams <[hidden email]> wrote:

>
> on Mon Jul 18 2011, Vicente Botet <vicente.botet-AT-wanadoo.fr> wrote:
>
>>
>> Hi Lorenzo,
>>
>> I don't remember what N1962 says, but I would force that preconditions and
>> post conditions evaluation shall not throw. If an exception is throw during
>> precondition evaluation, post-condition preparation or evaluation I would
>> say the program should terminate, as the program can not state if the
>> conditions are satisfied or not.
>
> That doesn't make any sense to me.  If you run out of memory while
> evaluating a precondition, it means you can't evaluate the precondition,
> not that the program can't recover.
>
> My guidelines are:
>
> - Use exceptions for recoverable conditions.
>
> - Do not use exceptions for non-recoverable conditions
>
> - Failure to satisfy a precondition is a program bug
>
> - Program bugs are non-recoverable
>
> - Anticipated failure to satisfy a postcondition (e.g. I can't get
>  enough memory to do my job) is a recoverable condition

Yes agreed but I'm sorry I managed to confuse everyone with this post
because I meant to ask something different...

Part of the issue might be that when someone mentions exceptions and
Contract Programming together the discussions if a contract failure
shall terminate the program or throw an exception starts almost
automatically... However, my question was NOT about throwing or
terminating in case of a contract failure. In case of a contract
failure, Boost.Contract calls the contract broken handlers which by
default call std::terminate (unless the user redefines the handlers to
do something else-- which could be to throw an exception, or print a
message, or play a sound, or anything the user wants to do). This is
exactly what N1962 specifies. In addition, the contract broken
handlers (and therefore std::terminate by default) are called if an
exception is thrown while checking a contract assertion.

My question instead, is: What shall I do if I fail to copy an oldof
value? Specifically, what shall I do if an oldof copy throws an
exception? This is not specified by N1962 (as far as I can see). I
decided that if I fail to copy and olfof value then I call the
postcondition_broken handler but only after executing the body (even
if oldof values are internally copied before the body is executed). I
am personally satisfied with this approach (letting the exception fly
out for the function would also be kind of OK but I didn't like it as
much because the caller might have no sense of the "new" exception
that is thrown only when contract code, the oldof, is evaluated and
never by the body itself).

For example, for std::vector::push_back:

    CONTRACT_FUNCTION_TPL(
    public void (push_back) ( (T const&) vlaue )
        postcondition(
            auto old_size = CONTRACT_OLDOF size(), // (1)
            size() == old_size + 1 // (2)
        )
    ) ;

If (2) evaluates to false, the postcondition_broken() function is
called. If an exception is thrown while checking (2),
postcondition_broken() is also called. postcondition_broken() will
just call std::terminate() however the user can redefined it assigning
a different function to the postcondition_broken() handler using
set_postcondition_broken(). All of this is in accordance with N1962
(as far as I understand it).

Now, my question is: What shall I do if an exception if thrown while
evaluating (1)? I have decided to still call postcondition_broken().

In either cases of (1) or (2) failing, postcondition_broken() is
always called after the body is executed. However, (1) is internally
evaluated before the body while (2) is evaluated after the body.

Thanks to all for your inputs and I hope I was able to clarify my question...

--Lorenzo
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

Dave Abrahams

on Tue Jul 19 2011, Lorenzo Caminiti <lorcaminiti-AT-gmail.com> wrote:

>
> I'm sorry I managed to confuse everyone with this post
> because I meant to ask something different...
>
> My question instead, is: What shall I do if I fail to copy an oldof
> value?

I don't think I misunderstood your question, although I don't happen to
know what "oldof" means here...

> Specifically, what shall I do if an oldof copy throws an
> exception? This is not specified by N1962 (as far as I can see). I
> decided that if I fail to copy and olfof value then I call the
> postcondition_broken handler but only after executing the body (even
> if oldof values are internally copied before the body is executed).

As I said, that doesn't make any sense to me, for the reasons I already
gave, and because failure to allocate memory in precondition checking
does not amount to a broken postcondition.

That said, the function itself might be a nothrow function and turning
on contract checking should not change the function's semantics.  That
would be my only argument against throwing an exception.

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

lcaminiti
Dave Abrahams wrote
on Tue Jul 19 2011, Lorenzo Caminiti <lorcaminiti-AT-gmail.com> wrote:

>
> I'm sorry I managed to confuse everyone with this post
> because I meant to ask something different...
>
> My question instead, is: What shall I do if I fail to copy an oldof
> value?

I don't think I misunderstood your question, although I don't happen to
know what "oldof" means here...

> Specifically, what shall I do if an oldof copy throws an
> exception? This is not specified by N1962 (as far as I can see). I
> decided that if I fail to copy and olfof value then I call the
> postcondition_broken handler but only after executing the body (even
> if oldof values are internally copied before the body is executed).

As I said, that doesn't make any sense to me, for the reasons I already
gave, and because failure to allocate memory in precondition checking
does not amount to a broken postcondition.
But in this case the failure is in allocating memory to copy an old value and NOT in checking preconditions.

Failing to copy an old value (e.g., for an alloc failure) will indeed not allow to check postconditions because the postconditions use the old value. Therefore, the postconditions should be considered failed because they cannot be checked and postcondition_broken should be called.

All of this reasoning does not have anything to do with the preconditions but only with the postconditions. Old-of values are part of (i.e., they are specified and used by) the postconditions (even if they are internally evaluated before the body and after the eventual preconditions).

For example (following N1962 proposed syntax):

    void push_back(T const& value)
        postcondition {
            size() == oldof size() + 1;
        }
    {
        vector_.push_back(value);
    }

Will be effectively implemented by something like this (ignoring class invariants for simplicity):

    void push_back(T const& value) {
        // eventual preconditions will be checked here

        bool oldof_failed = false;
        size_type old_size;
        try {
            old_size = size(); // old-of copy
        } catch(...) {
            oldof_failed = true;
        }

        // the body can be called here (regardless of oldof_failed) because precondition passed
        vector_.push_back(value); // body

        try {
            if(oldof_failed) throw runtime_error("old-of failed");
            if(!( size() == old_size + 1 )) throw logic_error("postcondition failed");
        } catch(...) {
            postcondition_broken(); // will call std::terminate (by default)
        }
    }

Where:

    void default_handler() { std::terminate(); }
    typedef void (*broken_handler)();
    broken_handler postcondition_broken = &default_handler;
    void set_postcondition_broken(broken_handler h) { postcondition_handler = h; }

You can redefine postcondition_broken to be smart and say "if there is an active exception that indicates the failure was because of an old-of copy then free some memory and signal the caller to retry the push_back call, else call std::terminate".

That said, the function itself might be a nothrow function and turning
on contract checking should not change the function's semantics.  That
would be my only argument against throwing an exception.
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

Dave Abrahams

on Tue Jul 19 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:

> Dave Abrahams wrote:
>>
>> on Tue Jul 19 2011, Lorenzo Caminiti <lorcaminiti-AT-gmail.com> wrote:
>>
>>>
>>> I'm sorry I managed to confuse everyone with this post
>>> because I meant to ask something different...
>>>
>>> My question instead, is: What shall I do if I fail to copy an oldof
>>> value?
>>
>> I don't think I misunderstood your question, although I don't happen to
>> know what "oldof" means here...
>>
>>> Specifically, what shall I do if an oldof copy throws an
>>> exception? This is not specified by N1962 (as far as I can see). I
>>> decided that if I fail to copy and olfof value then I call the
>>> postcondition_broken handler but only after executing the body (even
>>> if oldof values are internally copied before the body is executed).
>>
>> As I said, that doesn't make any sense to me, for the reasons I already
>> gave, and because failure to allocate memory in precondition checking
>> does not amount to a broken postcondition.
>>
>
> But in this case the failure is in allocating memory to copy an old value
> and NOT in checking preconditions.
>
> Failing to copy an old value (e.g., for an alloc failure) will indeed not
> allow to check postconditions because the postconditions use the old value.
> Therefore, the postconditions should be considered failed because they
> cannot be checked and postcondition_broken should be called.

No (IMO).  postcondition_broken indicates a program bug.  As I mentioned
in my guidelines, anticipated failure to satisfy a postcondition is a
recoverable condition and should normally result in an exception.

Of course, if that would change the contract of the function, it's
unacceptable ;-)

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] oldof failure not in N1962?

lcaminiti
On Tue, Jul 19, 2011 at 5:41 PM, Dave Abrahams <[hidden email]> wrote:

>
> on Tue Jul 19 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:
>
>> Dave Abrahams wrote:
>>>
>>> on Tue Jul 19 2011, Lorenzo Caminiti <lorcaminiti-AT-gmail.com> wrote:
>>>
>>>>
>>>> I'm sorry I managed to confuse everyone with this post
>>>> because I meant to ask something different...
>>>>
>>>> My question instead, is: What shall I do if I fail to copy an oldof
>>>> value?
>>>
>>> I don't think I misunderstood your question, although I don't happen to
>>> know what "oldof" means here...
>>>
>>>> Specifically, what shall I do if an oldof copy throws an
>>>> exception? This is not specified by N1962 (as far as I can see). I
>>>> decided that if I fail to copy and olfof value then I call the
>>>> postcondition_broken handler but only after executing the body (even
>>>> if oldof values are internally copied before the body is executed).
>>>
>>> As I said, that doesn't make any sense to me, for the reasons I already
>>> gave, and because failure to allocate memory in precondition checking
>>> does not amount to a broken postcondition.
>>>
>>
>> But in this case the failure is in allocating memory to copy an old value
>> and NOT in checking preconditions.
>>
>> Failing to copy an old value (e.g., for an alloc failure) will indeed not
>> allow to check postconditions because the postconditions use the old value.
>> Therefore, the postconditions should be considered failed because they
>> cannot be checked and postcondition_broken should be called.
>
> No (IMO).  postcondition_broken indicates a program bug.  As I mentioned
> in my guidelines, anticipated failure to satisfy a postcondition is a
> recoverable condition and should normally result in an exception.
>
> Of course, if that would change the contract of the function, it's
> unacceptable ;-)

I see your point... what to do if contract checking (including old-of
copies) throws an exception is a debatable point (also mentioned in a
previous rev of N1962).

However, if you decide to throw the contract exception outside the
called function there are a couple of important issues to keep in
mind:
1) The caller might not except such an exception because is not among
the ones the body throws. You already mentioned the extreme case of
throwing an alloc error because of an old-of copy failure for a body
that does not throw (throw() exception spec)-- the caller will handle
no exception because of the throw() spec of the body.
2) The exception might be thrown when checking class invariants at
destructor entry so the destructor execution will throw violating STL
exception safety rules.

To address 2), N1962 finally decided to:

``
It is always called as if surrounded by a try-catch block:

try
{
    class_invariant();
}
catch( ... )
{
    std::class_invariant_broken();
}
rationale: this ensures that exceptions thrown in the invariant cannot
escape from functions and in particular not from the destructor. [6]
``

In other words, an exception thrown by class invariant checking will
call the class invariant broken handler. I think the best and most
consistent why to handle the more general issue of exceptions thrown
while checking a contract is to always call the broken handlers (so
not just for class invariants but also for preconditions,
postcondition, static class invariants, block invariants, and loop
variants). Note that this neither terminates nor throws, it simply
calls the handlers that only by _default_ terminate.

Note that in Boost.Contract you can redefine the broken handlers to
re-throw exceptions not thrown by a contract condition failure (e.g.,
a runtime_error) but to still terminate otherwise therefore achieving
the behavior you described (you will need to pay special attention to
destructors). For example, set the broken handlers to:

void david_handler(from const& context) {
    try {
        throw; // re-throw to handle active exception
    } catch(contract::broken& condition_failure) {
        // a contract condition was evaluate false, it's a bug terminate
        std::terminate();
    } catch(...) {
        // some other hopefully recoverable error (alloc, etc),
rethrow unless from destructor entry
        if(context == FROM_DESTRUCTOR) std::terminate();
        else throw; // exception will fly out to the caller
    }
}

set_precondition_broken(&david_handler);
set_postcondition_broken(&david_handler);
set_class_invariant_broken(&david_handler);
set_block_invariant_broken(&david_handler);
set_loop_variant_broken(&david_handler);

Here, 2) is explicitly addressed by terminating for destructors all
the times. While 1) should no longer be a concern because if
programmers redefine the handlers to throw it makes sense that they
also program the callers to handle exceptions thrown by the contracts
even if the body is known to not throw them (based on its exception
specifications, documentation, or similar).

In summary, while I have seen this issue debated both ways, I think
the concept "the contract broken handler is called unless the contract
condition is evaluated to be true" is clear and simple (this includes
the case of a contract condition evaluated to be false, an
unercoverable? bug, but also a contract condition that cannot be
evaluated because it throws, a recoverable? error). At the end,
programmers can configure the broken handlers to take the actions they
need (in fact, in some applications even a bug might be better handled
by starting a "return home" procedure instead of terminating the
program).

I will add this example to the docs.

Thanks,
--Lorenzo
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost