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

Subject: Re: [boost] [contract] oldof failure not in N1962?
From: Vicente Botet (vicente.botet_at_[hidden])
Date: 2011-07-18 17:01:58

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

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