2012/6/12 lcaminiti <lorcaminiti@gmail.com>
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 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_...
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?