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

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-06-13 07:07:08

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

>
> Andrzej Krzemienski wrote
> >
> > I am trying to understand how the feature of relaxing preconditions in
> > overridden functions work or should work. Given the situation, where I
> > call
> > an overridden function via base class reference:
> >
> > *struct Base
> > {
> >   virtual void fun(bool b) = 0 precondition{ b == true };
> > };
> >
> > struct Deriv : Base
> > {
> >   void fun(bool b) override precondition{ true };
> > };
> >
> > void test( Base & b )
> > {
> >   b.fun(false); **// broken contract or not?**
> > }*
> >
> > Should this be treated as a broken contract or not? My reading of  the
> > documentation says that contract is not broken (because the
> >
>
> If b.fun(false) is valid or not depends by the actual object referenced by
> b
> (?!). For example:
>
> Deriv d;
> test(d);
>
> This passes because the subcontracted precondition of d.func(false) is
> `true or (false == true)` which is true. However if:
>
> struct Deriv2 : Base
> {
>  void fun(bool b) override precondition{ false };
> };
>
> Deriv2 d2;
> test(d2);
>
> This fails because the subcontracted precondition of d2.func(false) is
> `false or (false == true)` which is false.
>
> This is how the library is implemented, however, is this a correct
> implementation of the substitution principle
> http://en.wikipedia.org/wiki/Liskov_substitution_principle? Or should this
>
> void test( Base & b )
> {
>   b.fun(false); **// broken contract or not?**
> }*
>
> always and just check the precondition of base::fun?
>
> 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.

> "logic-or&lt;
> http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_0/doc/html/contract__/contract_programming_overview.html#logic_or_anchor&gt
> ;"
> > logic applies), but I feel that whoever implemented function *test *made
> a
> > mistake: he cannot assume what type will be implementing "interface"
> > *Base*,
> > so he cannot rely on the precondition being relaxed (even if he gets away
> > with it this time).
> >
>
> If you find this confusing, welcome to the club ;) N1962 prohibits
> overriding preconditions "even if subcontracting is theoretically sound and
> based on substitution principle, precondition can only be defined by base
> classes...". I find overriding preconditions also confusing.
>
> My library allows you to prohibit subcontracted preconditions like N1962
> specifies by defining the configuration macro
> CONTRACT_CONFIG_DO_NOT_SUBCONTRACT_PRECONDITIONS (however, in case of
> multiple inheritance preconditions of all base classes are still checked in
> logic-or with respect to each other, N1962 does not discuss this case
> explicitly...).
>
> 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.

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
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
technically, you can define two completely unrelated preconditions in
overriding and overridden function. In your example with 'integral' and
'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?