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 17:50:58

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

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