On Sun, Apr 11, 2010 at 7:49 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> 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@cs.aau.dk> 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@cs.aau.dk> 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.
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
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 ** 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