Re: [boost] [contract] relaxing preconditions in subcontracting

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-06-14 06:57:35

2012/6/13 lcaminiti <lorcaminiti_at_[hidden]>

> > suggestion. I read in
> > http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html that
> > you
> > can only relax preconditions; that is, you mustn't make them stronger.
> The
> > issue I see with this is that the "mustn't" is left entirely to the good
> > will of the derived class designer and never checked by anyone. So
> >
>
> I don't think that is correct. In fact, there's no way the derived class
> designer can strength a base class precondition because the base class
> precondition is checked in logic-or. For dervied::f the subcontracted
> preconditions are:
>
> derived::f::subcontracted_pre := base::f::pre or derived::f::pre
>
> This is always true when base::f::pre is true and regardless of
> dervied::f::pre so the subcontracted precondition cannot be stronger (more
> demanding, false when the base is true) no matter what the derived class
> designer does with derived::f::pre. In fact, subcontracting allows the base
> class designer to always remain in control as the base class contract
> (precondition, postconditions, and class invariants) must always be
> satisfied by all derived classes no matter how you design the derived
> classes. (Of course, if you don't use the library macros do define the
> derived class then you're on your own, there's no way my library can
> enforce
> anything.)
>
> IMO, a real good subcontracting example is:
>
> http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_0/doc/html/contract__/tutorial.html#contract__.tutorial.inheritance_and_subcontracting
>

This is a bit off topic, but I think there is something wrong with the
postconditions of unique_identifiers::add(). If you require that the added
indentifier must not be in the collection yet, why should you check in the
postcondition if it was there before the addition: it is obvious it wasn't.

> Keeping in mind the substitution principle:
> http://en.wikipedia.org/wiki/Liskov_substitution_principle
> If derived::f overrides base::f then derived::f must be used wherever
> base::f is used. Where base::f can be called, derived::f can be called. So
> where base::f preconditions are true, also derived::f (subcontracted)
> preconditions are true. That is ensured by subcontracting using the
> logic-or:
>
> derived::f::subcontracted_pre := base::f::pre or dervied::f::pre
>
> This is always true where base::f::pre is true so it always OK to call
> dervied::f where it was OK to call base::f (as the substitution principle
> says).
>

I think we interpret the "substitution principle" somewhat differently
(tell me, if I am wrong). My interpretation is, that it is the author of
the derived class (and the relaxed preconditions) that is responsible for
making sure that certain semantic constraints are met -- not your
framework. Overriding the preconditions so that they are not relaxation of
base preconditions is such a semantic error made by the author of the
derived class. Your framework makes the (successful) effort to work around
this error (using the logic-or), but I believe it is not the right thing to
do. The whole purpose of the concept of DbC (apart from documentation) is
to detect any "logic" errors at run-time,report them, and ideally prevent
the further execution of the program. The logic-or appears to me like doing
exactly the opposite: hiding a logic error. Even if other frameworks in
Eiffel or D do it this way, I would dare to say that they are doing it
wrong.

> 'natural' it is stressed that one should not derive one type from another,
> > but when it comes to preconditions the problem is that the precondition
> in
> > overriding function is not relaxed but in fact more constrained. This is
> > the bug that your library could help detect. Of course it is not possible
> > to assert in general that one predicate represents a relaxation of
> > another,
> > but what you could do is, when you check preconditions and find that the
> > overriding precondition failed but the overridden precondition passed,
> > signal this at run-time as design error. In other words:
> >
> > if (neither base nor derived precondition holds) {
> >    report precondition violation
> > }
> > else {
> >   if (derived precondition fails but base precond holds) {
> >     report "precondition design" error
> >   }
> >   else {
> >     precondition is satisfied
> >   }
> > }
> >
> > Or perhaps your library already works like that?
> >
>
>
> This would be easy to implement because my library internally goes over
> nested if statements like the one above when evaluating subcontracted
> preconditions. However, IMO having yet another configuration macro to
> enable
> detecting this case and explaining this case to the user complicates the
> situation even more. Again, I think this design is simpler and sufficient
> for the user "if you want to deal with subcontracted preconditions then
> they
> are as from the substitution principle (and Eiffel), otherwise you can
> disable subcontracted preconditions all together".
>

You are probably right that since the relaxation of preconditions is likely
not to be usefull at all, making too much effort to have it work this way
or the other, is not the economically correct way to go. Assuming that the
implementation of Boost.Contract (didn't see it yet) is as thorough as its
documentation, I can only imagine how much effort you must have put into
it, and still will have to.

It is an impressive piece of work.

Regards,
&rzej