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 17:43:18

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

>
> >> 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.
> >
>
> I'll clarify this in the docs, but there's nothing wrong with guarding a
> postcondition with its precondition. On the contrary, a function promises
> to
> satisfy its postconditions only when its preconditions were satisfied
> before
> body execution. Because subcontracted preconditions are checked in
> logic-or,
> overridden postconditions can be checked even if the related overridden
> preconditions were false (because the overriding preconditions are true and
> subcontracted preconditions are checked in logic-or). So guarding a base
> function postconditions with its preconditions allows the base class
> designer to program the fact that "the base function postcondition are
> ensured to be true only when the base function precondition are true". That
> gives the derived class designed more flexibility because he/she doesn't
> have to program the derived function to satisfy the base function
> postcondition under cases that satisfy the derived preconditions but not
> the
> base preconditions.
>
> base::f::pre := (pre1)
> base::f::post := (pre1 ? post1 : true)
>
> derived::f::pre := (pre1) or (pre2) // automatic `or` from subcontracting
> derived::f::post := (pre1 ? post1 : true) and (post2) // automatic `and`
> from subcontracting
>
> 1) base::f::pre must always satisfy post1 because it is valid to call it
> only when pre1 (preconditions) is true in which case post1 must be true too
> (postconditions).
>
> 2) However, derived::f does not have to always satisfy post1. If derived::f
> is called with pre1 false and pre2 true the call is valid because the
> subcontracted preconditions are:
>
> (pre1) or (pre2) == (false) or (true) == true)
>
> The subcontracted postconditions are (note that post1 disappears):
>
> (pre1 ? post1 : true) and (post2) == (false ? post1 : true) and (post2) ==
> (true) and (post2) == post2
>
> When pre1 is false, dervied::f does not to satisfy the overridden
> postcondition post1, just post2 is ensured!
>
> Note that this is possible only because the base class designer guarded
> post1 with pre1 so the base class designer is always in control and he/she
> can freely chose if to program guarded postconditions that can be
> "disabled"
> by derived classes so to grant derived class designers more flexibility. By
> default, that flexibility is not there in subcontracting that evaluates
> postconditions in logic-and, unless the base class designers intentionally
> guards its postconditions.
>
> I thought this was a nice trick from [Micthell02] that shows how
> subcontracting preconditions might actually be of some use (but the logic
> it's tricky to follow and it might be confusing so if programmers don't
> need
> this they can disable it with the configuration macros and as required by
> N1962). Note that N1962 authors mentioned on this ML that they looked at
> extensive Eiffel code and talked with Eiffel programmers only to find out
> that no one actually uses subcontracted preconditions in practice. So all
> this might be of little practical interest.
>

Ok, I get it now. Thanks for taking the time to explain that. Now I also
see what you meant by "confusing" the other day.

>
> >> 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
> >
>
> AFAIU, the substitution principle means that the Contract Programming
> methodology (and it's implementation in my library) should ensure the
> following:
>

I am trying to identify where precisely we disagree. I am not sure if this
is just a matter of opinion. I do not think that "Contract Programming
methodology [...] should ensure" anything. I have read the link you sent,
and this is what I understand: A programmer John may (or may not) choose to
write his program using the "Contract Programming methodology". If he does
so, he is bound to obey some rules, one of such rules being that
"subcontracted" preconditions cannot be strengthened. -- John must make sue
that this happens. The role of the framework as yours -- as I see it (but I
might be wrong) -- is to help _verify_ if John did his job right. That is,
the job of your framework is somewhat "negative": you should be looking for
mistakes and pointing them out; be a pain for the programmer (hence the
default behavior of terminating the program). If John makes a mistake and
over-constrains the precondition in the overridden method and you apply the
logic-or, his mistake will never be revealed.

>
> From: http://en.wikipedia.org/wiki/Liskov_substitution_principle
>
> Liskov and Jeannette Wing formulated the principle succinctly in a 1994
> paper as follows:
>
> "Let q(x) be a property provable about objects x of type T. Then q(y)
> should
> be provable for objects y of type S where S is a subtype of T."
>
> In the same paper, Liskov and Wing detailed their notion of behavioral
> subtyping in an extension of Hoare logic, which bears a certain resemblance
> with Bertrand Meyer's Design by Contract in that it considers the
> interaction of subtyping with pre- and postconditions.
> ...
> These are detailed in a terminology resembling that of design by contract
> methodology, leading to some restrictions on how contracts can interact
> with
> inheritance:
> 1. Preconditions cannot be strengthened in a subtype.
> 2. Postconditions cannot be weakened in a subtype.
> 3. Invariants of the supertype must be preserved in a subtype.
>
> 1. is implemented by checking subcontracted preconditions in logic-or with
> each other. 2. and 3. by checking subcontracted postconditions and class
> invaraints in logic-and.
>
>
>
> > 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
> >
>
> I think it is the Contract Programming responsibility to check and enforce
> the subcontracting semantic, and not the derived class designer. Note that
> when you program subcontracted preconditions, postconditions, and
> postconditions, you are not just programming assertions for the derived
> class in isolation from the base classes (just like when you implement a
> derived class you don't do that without considering the implications of
> inheriting from the base classes -- e.g., inherited members, etc).

Agreed that when constraining derived class John has to consider the
constraints of the base class, but still having considered this he has to
state his constraints correctly. Well, let me show by example what I mean:

void Base::fun( int i ) precondition{ i > 0; }
void Derived::fun( int i ) precondition{ i == 0; }

The two conditions are completely unrelated, and to me, it is John's logic
error to have put conditions like that. I can imagine now circumstances
(e,g, some postconditions, or invariants, or whatever context) where such
definition could be considered correct (am I wrong?). But if logic-or is
guaranteed, you can treat the subcontracted precondition as valid one,
which in contrived way says that (i >= 0). But it feels wrong to allow John
saying his intentions this way. The framework should (this is how I see it)
force John to state the precondition i >= 0 explicitly rather than the
condition being "collected" from the inherited preconditions.

But this is just one point of view, I guess.

Regards,
&rzej