Re: [boost] [contract] diff n1962

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

Hello,

On Fri, Apr 9, 2010 at 7:57 AM, Thorsten Ottosen <nesotto_at_[hidden]> wrote:
> Lorenzo Caminiti skrev:
>> 1) SUBCONTRACTING
>> n1962 allows only the base class to specify preconditions. Instead,
>> Boost.Contract allows also derived classes to specify preconditions.
>> ...
>> Why does n1962 allow preconditions only for the base classes?
> ...
> I investigated a large Eiffel library and found that the feature wasn't
> really used. I could come up with zero /realistic/ use-cases, and so we
> thought it was better to leave it out.

This is an example of how overriding preconditions allows
relaxed_name_list::put() to relax his parent's name_list::put()
constraint that names cannot be duplicated in the list:
    http://dbcpp.sourceforge.net/example/Mitchell2002/name_list/names.hpp
However, this is an academic example and not a realistic one. While I
think it is conceivable some programmers would actually want to
override preconditions, I cannot offer any realistic example -- within
the ~60,000 lines of C++ project I work one, we essentially never used
this feature.

That said, I would leave this feature in Boost.Contract so people can
experiment with it -- and perhaps come up with a realistic use case. I
do understand the importance of a realistic use case if this feature
were to be added for language support.

>> 2) STATIC CLASS INVARIANTS
>> n1962 does not support static class invariants. Instead,
>> Boost.Contract supports static class invariants.
>> ...
>> Why does n1962 not support static class invariants?
> ...
> It never occurred to us that (subsets of) global variables
> should have their own invariant. Again, how common is this?

Also for this feature I cannot provide any realistic use case. In the
~60,000 lines of C++ project I work one, we never use static class
invariants -- but we never even use static variables neither, we only
use static const variables, so I am not sure how much can be concluded
from that.

Again, I would leave static class invariants in Boost.Contract for
people to experiment with it (but I understand the need for real use
cases if this were to be requested for language support).

>> 5) CONTRACT CHECKING ORDER (policy)
>> n1962 checks contracts as pre > inv > body > inv > post. Instead,
>> Boost.Contract checks contracts as inv > pre > body > inv > post,
>> where inv is static-inv > non-static-inv.
> ...
> I think what is needed is a dead-good realistic example from real
> code. In some sense the initial check for the invariant is
> redundant, because it will always have been performed in the constructor or
> at the end of a nother function. We have it there as an additional
> debugging help, nothing else.

Yes, but private member functions (and in case of Boost.Contract any
member function, including public ones, without a contract) could have
broken the invariant making the extra debugging invariant check even
more useful. There might be a real example of this in the ~60,000
lines of C++ project I work one... it is a difficult analysis to
conduct but I will keep an eye open for it.

>> 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?

> HTH

Yes, your comments as well as n1962 and all your previous CP proposal
revisions have been of great help. Thank you very much.

Lorenzo