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

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2012-06-14 14:29:23

Andrzej Krzemienski wrote
> 
> 2012/6/13 lcaminiti <lorcaminiti@>
> 
>> > 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.
> 

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.

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

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). Eiffel
stresses this out also syntactically using different keywords for
subcontracted preconditions `ensure else` (else = logic-or) and for
subcontracted postconditions `require then` (then = logic-and). Eiffel will
give you an error if you use `ensure` or `require` instead of `ensure else`
or `require then` for a derived class function that is overriding a base
class function.

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

OK, now I'm going to brag a bit about my library ;) The docs are like an
after-thought compared to the implementation. There are 289 source files for
32,286 lines of code of which 80% is preprocessor meta-programming. I
wouldn't be surprised if this is one of the most extensive (ab)use of the pp
ever! The programming required to parse the syntax (using pp), handle
subcontracting (using pp and later introspection), and handle the `=` symbol
in the `old_var = CONTRACT_OLDOF expr` (using pp, TMP, type deduction,
default function parameters with initialization, and more) were quite a
trip.

But after all of this (fun) stuff that taught me a lot of C++, the real
question still stands: will anyone ever find this library useful??

Ciao.
--Lorenzo

--
View this message in context: http://boost.2283326.n4.nabble.com/contract-relaxing-preconditions-in-subcontracting-tp4631177p4631304.html
Sent from the Boost - Dev mailing list archive at Nabble.com.