Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-15 10:27:47

On Wed, Apr 14, 2010 at 4:50 PM, Thorsten Ottosen <nesotto_at_[hidden]> wrote:
> Lorenzo Caminiti skrev:
>>
>> On Sun, Apr 11, 2010 at 7:49 PM, Lorenzo Caminiti <lorcaminiti_at_[hidden]>
>> wrote:
>>>
>>> Agreed: the most constructive way to discuss policies 6) and 7) is for
>>> me to present examples. I will work on this.
>>
>> I checked that the current Boost.Contract implementation follows the
>> policies 6) and 7) as originally specified in n1613 (the original
>> revision on n1962). I would like to ask for additional clarifications
>> on the rational for changing (relaxing) these policies in subsequent
>> revisions of the CP C++ standard proposal.
>
>>
>> Revision history for 6) "disabling of checks during assertions":
>>    yes, but not in preconditions -- n1962 ** latest proposal revision **
>>    no -- n1866, n1773
>>    yes -- n1669, n1613 ** current Boost.Contract **
>>
>>> From n1613: <<There is one global rule about assertions and it is that
>>
>> assertions must
>> be disabled in assertions. This removes the possibility of infinite
>> recursion
>> and allows a reasonable performance even with assertions enabled. With-
>> out disabling assertions, infinite recursion will happen when a public
>> func-
>> tion appears in the invariant.>>
>> This is also the policy that Eiffel follows.
>
> First of, the problem is not so big IMO. If your tests runs all functions,
> the infinite recursion is easy to detect and fix.
>
> D disables nothing, which we found somewhat silly since it is
> merely leading to poorer performance in debug-builds and adds cheks that
> are unlikely to recove any real errors (it deals mostly with "second hand
> errors").
>
> Preconditions, OTOH, need to be checked to ensure correctness.

I understand. Checking for correctness is the main objective of
Boost.Contract so I will change the library to not disable any
assertion checking in preconditions. Unless there are objections, I
will also provide a configuration macro
CONTRACT_CONFIG_DISABLE_ASSERTION_CHECKING_IN_PRECONDITION (default
value 0) for programmers that are more concerned with the infinite
recursion issue.

Is there a code example of how
CONTRACT_CONFIG_DISABLE_ASSERTION_CHECKING_IN_PRECONDITION=1 will
brake correctness? I would like to add it to the library
documentation.

> On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto_at_[hidden]> wrote:
>>> 7) NESTED FUNCTION CALLS (policy)
>>> n1962 disable nothing. Instead, Boost.Contract disables invariant
>>> checking within nested function calls.
>>>
>>> I found this policy useful to prevent infinite recursion. Previous
>>> revisions of n1962 (n1613) specified the Boost.Contract policy. Eiffel
>>> disables all checks (not just invariants). Boost.Contract could be
>>> changed to comply with n1962.
>>>
>>> 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 do not fully understand this... is there a code example?

> Revision history for 7) "when public func. call public func.":
>    disable nothing -- n1962, n1886, n1773 ** latest proposal revision **
>    disable invariant -- n1669, n1613 ** current Boost.Contract **
>
> From n1613: <<When calls to public member functions are nested, the
> invariant is not
> checked before and after the inner call. This is because the invariant is al-
> lowed to be temporarily broken within a call to a public function. The other
> contracts of the functions must still be checked though (see also section 7 on
> page 18).>>

Is this still true? If yes, how does it reconcile with the issue above
of the callee not knowing if the invariant has been established by the
caller?

Thank you very much.
Lorenzo