Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-14 14:40:24

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.

On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto_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.
>>
>> I found this policy useful to prevent infinite recursion. Previous
>> revisions of n1962 (n1613) specified the same policy implemented by
>> Boost.Contract. Furthermore, Eiffel implements the Boost.Contract
>> policy. Boost.Contract could be changed to comply with n1962.
>>
>> 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.

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.

Does n1962 policy introduce the opportunity for infinite recursion? For example:

    class x {
        CONTRACT_CLASS( (x) )

        CONTRACT_FUNCTION(
        (bool) (g)( (int)(x) ) (const)
            (precondition) (
                ( f(x) )
            )
        ({
            return true;
        }) )

        CONTRACT_FUNCTION(
        (bool) (f)( (int)(x) ) (const)
            (precondition) (
                ( g(x) )
            )
        ({
            return false;
        }) )
    };

Call sequence without disabling assertions from preconditions:
    call x::f(x) -> check x::f(x) pre -> call x::g(x) -> check x::g(x)
pre -> x::f(x) (infinite recursion) ...
Call sequence disabling assertions when checking assertions (also for
preconditions):
    call x::f(x) -> check x::f(x) pre -> call x::g(x) -> return true
(x::g(x) precondition check is disabled, no infinite recursion) ->
x::f(x) body ...

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.

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).>>
Eiffel disables all checks (invariants, preconditions, and postconditions).

(I incorrectly stated this will lead to infinite recursion but that is
not the case based on 6). Therefore, I do not an infinite recursion
example for this.)

For both 6) and 7), note that it would be trivial to change
Boost.Contract to fully comply with n1962. I am honestly trying to
understand which policies are the best ones given that the different
C++ proposal revisions and Eiffel all seem to use somewhat different
specifications on this.

Thank you very much for your help.
Lorenzo