Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-11 19:49:34

On Sun, Apr 11, 2010 at 7:32 PM, vicente.botet <vicente.botet_at_[hidden]> wrote:
>>>> 6) DISABLE ASSERTION CHECKING WITHIN ASSERTIONS CHECKING (policy)
>>>> n1962 only disables assertion checking from within preconditions
>>>> checking. Instead, Boost.Contract disables assertion checking from
>>>> within all contract checking.
>>>> ...
>>>> Why does n1962 disable assertion checking only from within preconditions?
>>> ...
>>> You got it the wrong way. Preconditions /never/ disable anything.
>>> You can prove that if you do so, an incorrect parameter might
>>> be passed on to the function body.
>>
>> Yes, I see that now -- from n1962 section 11 <<disabling of checks
>> during assertions ... yes, but not in preconditions>>. Good thing I
>> checked...
>>
>> Eiffel disables checks also in preconditions to avoid infinite
>> recursion. I can change this in Boost.Contract but is there a concern
>> with infinite recursion?
>>
>>>> 7) NESTED FUNCTION CALLS (policy)
>>>> n1962 disable nothing. Instead, Boost.Contract disables invariant
>>>> checking within nested function calls.
>>>> ...
>>>> Why does n1962 not disable invariants checking in nested calls?
>>> ...
>>> Because the callee does not know if the invariant has been
>>> proper established by the caller. The caller cares about the invariant
>>> on entrance/exit, but now must also do so when calling another
>>> public function.
>>
>> I am not sure I understand, could you please provide an example?
>>
>> Similar to 6), Eiffel disables all checks in nested calls to avoid
>> infinite recursion. Once I understand this better, I could change this
>> in Boost.Contract but is there a concern with infinite recursion?
>>
>
> I don't see any problem with infinite recursion. Could you give an example?

Agreed: the most constructive way to discuss policies 6) and 7) is for
me to present examples. I will work on this.

(There were a couple of infinite recursion examples I encountered
while reading CP Eiffel code and developing the library, I will dig
that code up.)

Lorenzo