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

Subject: Re: [boost] [contract] oldof failure not in N1962?
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2011-07-18 15:32:20

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

--
View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-oldof-failure-not-in-N1962-tp3676021p3676201.html
Sent from the Boost - Dev mailing list archive at Nabble.com.