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

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2012-06-13 15:47:48

Andrzej Krzemienski wrote
> 
> 2012/6/12 lcaminiti <lorcaminiti@>
>> I'm honestly not sure, I need to think about it more and also check what
>> Eiffel does... I'll take that as a homework.
>>
> One option to consider is to apply different checking algorithm if our
> function is called via vtable and a different one when our overridding
> function is called directly.
> 

I'm afraid that will make subcontracted preconditions even harder to
understand and use. IMO, a very reasonable approach is to do what the
substitution principle says (which supposedly is also what Eiffel
implements) -- because that gives a theoretical rationale for subcontracting
in OOP. But at the same time provide a configuration macro to simplify
things -- because some programmers might find subcontracted preconditions
confusing and not useful in practice. That way both theoretical and
practical aspects of the Contract Programming paradigm are taken into
account.

>> I tried to document this in the Advanced Topics section:
>>
>> http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_0/doc/html/contract__/advanced_topics.html#contract__.advanced_topics.subcontracting_preconditions
>>
>> At the end, my library should:
>> 1) Implement what defined by the substitution principle (and implemented
>> by
>> Eiffel).
>> 2) But provide a configuration macro to avoid all this confusion by
>> generating a compiler error if you try to subcontract a precondition.
>>
>>
> 
> I believe your choice to give users the option to use relaxed
> preconditions
> or not is the best possible. In my opinion the primary benefit of the this
> library is to give people the tool to test DbC in practice, learn it and
> draw conclusions like "relaxed preconditions are useless" themselves.
> 

Yep, hopefully using the library people can experience the benefits of
programming program specifications and then we get these features in the
core language. From the Introduction section:

With the addition of contracts, concepts, and named parameters, C++ could
introduce formal program specification into main-stream programming. The
authors wish the work done in developing this library will persuade the C++
community and the C++ standard committee to add these features to the core
language so to support formal program specification without the unusual
macro syntax and avoiding high compilation times (unfortunately, this has
not been the direction taken for C++11 with the rejection of the concept
proposal [N2081] and the lack of consideration for the Contract Programming
proposal [N1962], but there might still be hope for C++1x with x > 1).

> I admit that I have little time to study your (very good) documentation
> thoroughly and to test the implementation, so sorry if I ask something
> that
> you already took effort to study and explain. But let me still share one
> 

No worries. Sorry the docs are quite extensive, but there's a lot of ground
to cover between contracts, concepts, and named parameters (it's like 3
libraries in 1)... but if you read the Contract Programming Overview and
Tutorial sections you should have a pretty solid understanding of what the
library can do as far as contracts go.

> 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

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

> technically, you can define two completely unrelated preconditions in
> overriding and overridden function. In your example with 'integral' and
> 

You can define unrelated preconditions in derived::f and base::f but the
library will automatically relate them via a logic-or as per subcontracting
and the substitution principle. Programmers don't have to relate the
preconditions, the library does that implementing subcontracting.

BTW, Eiffel uses the special keywords `require else` (subcontract
preconditions) and `ensure then` (subcontracted postconditions) to remind
programmers that they are writing preconditions in logic-or (else) and
postconditions in logic-and (then) with the overridden function.
http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_0/doc/html/contract__/contract_programming_overview.html#contract__.contract_programming_overview.features

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

Thanks.
--Lorenzo

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