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

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

'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-subcon... Sent from the Boost - Dev mailing list archive at Nabble.com.

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

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.

...

...

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

...

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

'natural' it is stressed that one should not derive one type from another, possible 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-subcon... Sent from the Boost - Dev mailing list archive at Nabble.com.

lcaminiti wrote

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.

I've checked and my current library implementation does what Eiffel does in this case. Consider the following Eiffel program: class B feature f ( b: BOOLEAN ) require b do print ("B%N") end end class D1 inherit B redefine f end feature f ( b: BOOLEAN ) require else True do print ("D1%N") end end class D2 inherit B redefine f end feature f ( b: BOOLEAN ) require else False do print ("D2%N") end end class APPLICATION inherit ARGUMENTS create make feature {NONE} -- Initialization test ( b: B ) do b.f (False) end make -- Run application. local d1: D1 d2: D2 do create d1 create d2 test(d1) -- OK: Subcontracted preconditions pass. test(d2) -- Error: Subcontracted preconditins broken. end end test(d1) passes the subcontracted preconditions while test(d2) does not. Therefore, the call b.f(False) passes the subcontracted preconditions if b is an instance of D1 (d1) but it does not pass the subcontracted preconditions if b is an instance of D2 (d2). My library does the same thing: #include <contract.hpp> CONTRACT_CLASS( struct (B) ) { CONTRACT_CLASS_INVARIANT( void ) CONTRACT_FUNCTION( public virtual void (f) ( bool b ) precondition( b ) ) { std::cout << "B" << std::endl; } }; CONTRACT_CLASS( struct (D1) extends( B ) ) { CONTRACT_CLASS_INVARIANT( void ) CONTRACT_FUNCTION( public void (f) ( bool b ) override precondition( true ) ) { std::cout << "D1" << std::endl; } }; CONTRACT_CLASS( struct (D2) extends( B ) ) { CONTRACT_CLASS_INVARIANT( void ) CONTRACT_FUNCTION( public void (f) ( bool b ) override precondition( false ) ) { std::cout << "D2" << std::endl; } }; void test ( B& b ) { b.f(false); } int main ( void ) { D1 d1; D2 d2; test(d1); // OK: Subcontracted preconditions pass. test(d2); // Error: Subcontracted preconditions broken. return 0; } Again, I understand how it can be confusing that the call b.f(false) is valid or not depending on the actual object referenced by b. Such a confusion comes from the fact that subcontracted preconditions are evaluated in logic-or (instead of logic-and) as I tried to explain the docs. However, I'd suggest for my library to: 1) Either, implement subcontracted preconditions as Eiffel does and in accordance to the substitution principle; 2) Or, disable subcontracted preconditions all together defining CONTRACT_CONFIG_DO_NOT_SUBCONTRACT_PRECONDITIONS in accordance with N1962. This way programmers can chose "I find subcontracted preconditions confusing... then I disable them at compile-time" or "I find subcontracted preconditions useful*... then I keep them and make them part of my design but I also fully study and understand them". (*) For example, a case where subcontracted preconditions _might_ be useful is when the base class designer want to grant greater control to the derived class designers using subcontracted preconditions and guarded postconditions (as I showed in a previous example for unique/multiple_identifiers taken from [Mitchell02]). But again, it's not clear if subcontracted preconditions have real practical value as noted in N1962. Thanks a lot. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/contract-relaxing-preconditions-in-subcon... Sent from the Boost - Dev mailing list archive at Nabble.com.