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

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2012-06-12 09:05:30

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.

> "logic-or<http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_0/doc/html/contract__/contract_programming_overview.html#logic_or_anchor>"
> 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.

Thanks,
--Lorenzo

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