Bug 6856 – Absence of in contract (precondition) on override of method that has one is badly designed

Precondition inheritance does not work in a satisfying way: import std.stdio; class A{ void foo()in{writeln("in!");}out{writeln("out!");}body{} } class B:A{ override void foo(){} // add in{assert(false);}body to get it working } void main(){ A x = new A; x.foo(); // in! \ out! B y = new B; y.foo(); // out! } If the child class does not specify an in contract on an overriding method, the in contract of the parent should be inherited, without adding a contract that always passes. The current behavior makes it too easy to inadvertently widen the interface and have undetected bugs. Chapter 10.9 in TDPL does not explicitly mention the fact that it is supposed to work that way, but it seems to assume it.

http://www.digitalmars.com/d/1.0/dbc.html "If a function in a derived class overrides a function in its super class, then only one of the in contracts of the function and its base functions must be satisfied. Overriding functions then becomes a process of loosening the in contracts. A function without an in contract means that any values of the function parameters are allowed." On an override, the semantics of an in contract are to _add_ to what is a legal call of the method. And the absence of an in contract in a function definition is really syntactic sugar for an empty in contract.

What about this: extern (C) int printf(char* s, ...); class X { void f() in { printf("\tX.f() in\n"); } body {} } class Y : X { override void f() in { printf("\tY.f() in\n"); } body {} } class Z : Y { override void f() body {} } void main() { printf("X x\n"); X xx = new X; xx.f(); printf("\t---\n"); printf("X y\n"); X xy = new Y; xy.f(); printf("\t---\n"); printf("X z\n"); X xz = new Z; xz.f(); printf("\t---\n"); printf("--------------------\n"); printf("Y y\n"); Y yy = new Y; yy.f(); printf("\t---\n"); printf("Y z\n"); Y yz = new Z; yz.f(); printf("\t---\n"); printf("--------------------\n"); printf("Z z\n"); Z z = new Z; z.f(); printf("\t---\n"); } It prints: X x X.f() in --- X y X.f() in --- X z --- -------------------- Y y X.f() in --- Y z --- -------------------- Z z --- Shouldn't "Y y" print "Y.f()" if Y can loose the in contract? Shouldn't "X z" and "Y z" print *something* (probably "X.f()" and "Y.f()" respectively)?

BTW, that was DMD 1.071.

BTW, "in" contracts seems to be very ill defined, because overriding a method with an "in" contract without specifying an "in" contract should inherit the contract from the base class/interface, not remove the contract completely. You have to repeat the contract from the base class manually, that sucks. There should be some syntax to remove the contract instead, maybe something like: void f() in delete body { // ... }

@Leandro: Your first example is okay. The precondition test shortcuts. It is more or less equivalent to passes(X_foo_in) || passes(Y_foo_in). If passes(X_foo_in), then the second part does not have to be evaluated, ergo it never prints "Y.f() in". The fact that in order to just inherit an in contract it is necessary to add an in{assert(0);} contract is hopefully just an oversight and not by design.

(In reply to comment #4) > BTW, "in" contracts seems to be very ill defined, because overriding a method > with an "in" contract without specifying an "in" contract should inherit the > contract from the base class/interface, not remove the contract completely. You > have to repeat the contract from the base class manually, that sucks. There > should be some syntax to remove the contract instead, maybe something like: > > void f() > in delete > body > { > // ... > } I think it should just look like this: override void f() in{}body{ // ... } If no explicit contract is added, it should be inherited.

OK, then the docs should be more clear I think, is really hard to infer this behavior from the docs (unless someone explains it better :).

(In reply to comment #2) > Shouldn't "Y y" print "Y.f()" if Y can loose the in contract? > Shouldn't "X z" and "Y z" print *something* (probably "X.f()" and "Y.f()" > respectively)? Only one of the contracts needs to pass for the overall contract to pass. So once it's tried one and found that it's passed, it doesn't need to try the others. When you have a Y, it first tries X's in contract. This passes, so it doesn't need to check Y's as well. Of course, an implementation could just as well check Y's contract first and then fall back to X's if that fails. But because Z's in contract is empty, the compiler just optimises away the whole contract checking.

(In reply to comment #8) > (In reply to comment #2) > > Shouldn't "Y y" print "Y.f()" if Y can loose the in contract? > > Shouldn't "X z" and "Y z" print *something* (probably "X.f()" and "Y.f()" > > respectively)? > > Only one of the contracts needs to pass for the overall contract to pass. So > once it's tried one and found that it's passed, it doesn't need to try the > others. > > When you have a Y, it first tries X's in contract. This passes, so it doesn't > need to check Y's as well. Of course, an implementation could just as well > check Y's contract first and then fall back to X's if that fails. > > But because Z's in contract is empty, the compiler just optimises away the > whole contract checking. I'm a little confused by the relationship between this bug and bug 6857. If you accept 6857, then if you call a function f() from a base class B, only the precondition of the base class should matter. Although one derived class C.f() may accept a weaker precondition, the caller doesn't actually know it had a C, so it's making an unwarranted assumption. So, if you accept that, then contracts in derived classes don't matter unless they are called directly. That's really odd, because you have a single function which has two different semantic guarantees depending on who is calling it. Following this through, I don't see the need for explicit widening of preconditions at all. If we didn't have the feature, and you needed it (which I believe happens very rarely), you could just create a separate function g() for the direct calls, and give _it_ the weaker contract. The derived function f() can just call g(). If you need to rely on the weaker contract, call g() instead of f(). Easy to implement, easy to understand. This explicit widening of preconditions of virtual functions seems to be a really niche feature.

(In reply to comment #9) > This explicit widening of preconditions of virtual functions seems to be a > really niche feature. I think it does makes some sense to be like this. You can see it as adding an extra method to a derived class, or class implementing an interface. The derived class adding a new method() still satisfies the interface, in the same sense an overriden method accepting wider preconditions still satisfies the original precondition, and the interface. The problem for me is: 1) The docs are not very clear about that. I didn't understood they worked like this until now, that some change in the compiler triggered an error on a "in" contract in Tango. I don't think I'm the only one misunderstanding contracts, as when I took a look at the code pre-conditions was wrongly used all over it. 2) There seem to be bugs in the implementation. For example in this Tango bug report: http://www.dsource.org/projects/tango/ticket/2067, the sync() method is OK to trigger the error because it comes from an interface with no preconditions, but the close() error seems to be wrong, as the parent class also has a precondition on that method. I didn't have the time to try to come up with a minimal testcase yet, sorry. Also, see this example: extern (C) int printf(char* s, ...); class X { void f(bool failx = false, bool faily = false) in { printf("\tX.f() in: assert(%d)\n", !failx); assert(!failx); } body {} } class Y : X { override void f(bool failx = false, bool faily = false) in { printf("\tY.f() in: assert(%d)\n", !faily); assert(!faily); } body {} } class Z : Y { override void f(bool failx = false, bool faily = false) in { printf("\tZ.f() in: assert(0)\n"); assert(false); } body {} } void main() { printf("--------------------\n"); printf("Z z\n"); Z z = new Z; z.f(true, true); printf("\t---\n"); } This is the output: -------------------- Z z Y.f() in: assert(1) --- Is there any good reason why suddenly faily gets set to false when true was passed? If this is confirmed as a bug I'll create another ticket.

Oh, and I think it will also make more sense to first check the subclass pre-condition (as it might be the wider one, and the one with more chances to pass) instead of the parent class, which is the more restrictive. I don't know if that's too hard to implement, and only a detail :)

(In reply to comment #10) > (In reply to comment #9) > > This explicit widening of preconditions of virtual functions seems to be a > > really niche feature. > > I think it does makes some sense to be like this. You can see it as adding an > extra method to a derived class, or class implementing an interface. Yes. But in those cases you mention, the syntax for accessing the base functionality is different to the derived functionality. But here we have something different: Derived c; Base b = c; c.foo(7); // OK b.foo(7); // fail -- precondition is not widened Same function body gets used in both calls, BUT different contracts need to get called. > The > derived class adding a new method() still satisfies the interface, in the same > sense an overriden method accepting wider preconditions still satisfies the > original precondition, and the interface. Yes, it does, but why is that desirable? When do you actually want that? Only in niche cases, I think.

(In reply to comment #12) > (In reply to comment #10) > > (In reply to comment #9) > > > This explicit widening of preconditions of virtual functions seems to be a > > > really niche feature. > > > > I think it does makes some sense to be like this. You can see it as adding an > > extra method to a derived class, or class implementing an interface. > > Yes. But in those cases you mention, the syntax for accessing the base > functionality is different to the derived functionality. But here we have > something different: > > Derived c; > Base b = c; > c.foo(7); // OK > b.foo(7); // fail -- precondition is not widened > > Same function body gets used in both calls, BUT different contracts need to get > called. I still don't see how that's wrong. I can understand it could be awful to implement. And I can even agree that it doesn't worth the trouble. But the code it self makes sense to me. > > The > > derived class adding a new method() still satisfies the interface, in the same > > sense an overriden method accepting wider preconditions still satisfies the > > original precondition, and the interface. > > Yes, it does, but why is that desirable? When do you actually want that? Only > in niche cases, I think. Yes, that's probably true. But if it's something easy to do, I see the sense on having the feature. If it's extremely hard I agree it might not worth it.

A's in must be executed only if B's in fails. in constract lossen themselves with override.

There is no "B's in". That is the point. The bug is that an implicit 'in' contract that always passes is added to B.foo.

(In reply to comment #15) > There is no "B's in". That is the point. The bug is that an implicit 'in' > contract that always passes is added to B.foo. Yes that is the point. As no contract has been specified, it is assumed that this function can accept anything. And so the implicit in contract alway succeed, so A's contract never get executed. Stewart Gordon already explained that and he is right. However, Don's proposal make sense (defining how contract is executed at callee's place instead of caller's place).

(In reply to comment #16) > (In reply to comment #15) > > There is no "B's in". That is the point. The bug is that an implicit 'in' > > contract that always passes is added to B.foo. > > Yes that is the point. As no contract has been specified, Wrong. The super class specifies a contract. This contract must be inherited. > it is assumed that this function can accept anything. That assumption is bogus, because this is almost never the case. It makes contract programming basically unusable. Such a strong weakening of the 'in' contract should not be the default. > And so the implicit in contract alway > succeed, so A's contract never get executed. > > Stewart Gordon already explained that and I understand all of this, and the fact that it works that way is a bug. > he is right. > He is right in that the implementation works that way. It shouldn't. > However, Don's proposal make sense (defining how contract is executed at > callee's place instead of caller's place). Don's proposal is to remove 'in' contract widening completely. That does not make a lot of sense to me.

(In reply to comment #17) > Don's proposal is to remove 'in' contract widening completely. That does not > make a lot of sense to me. Don's proposal is similar to what you reported here as issue 6857 , which make a lot of sense.

(In reply to comment #17) > That assumption is bogus, because this is almost never the case. > It makes contract programming basically unusable. Such a strong > weakening of the 'in' contract should not be the default. It depends on how you look at it. A function can, by default, accept any arguments of the types specified. I think the view taken is that the in contract supplements the parameter list, and the absence of an in contract with a given parameter list denotes an absence of further restrictions on what may be passed into the function. > Don's proposal is to remove 'in' contract widening completely. > That does not make a lot of sense to me. Indeed, it does seem that Don doesn't like contravariance.

(In reply to comment #19) > (In reply to comment #17) > > That assumption is bogus, because this is almost never the case. > > It makes contract programming basically unusable. Such a strong > > weakening of the 'in' contract should not be the default. > > It depends on how you look at it. I look at it in a pragmatic way. Have you ever used the feature in any language? > A function can, by default, accept > any arguments of the types specified. I think the view taken is that > the in contract supplements the parameter list, > and the absence of an > in contract with a given parameter list denotes an absence of further > restrictions on what may be passed into the function. > By symmetry, the view would have to be taken that the out contract supplements the return type. Do you see how that is problematic? Whatever reason for the current behavior there might be come up with when thinking hard about it: The current behavior of DMD is not useful, and I refuse to believe that it is by design. I am not aware of any language that specifies such non-useful semantics for their contract inheritance.

(In reply to comment #15) > There is no "B's in". That is the point. The bug is that an implicit 'in' > contract that always passes is added to B.foo. If I didn't supply an 'in' to the derived class function, I would expect not abiding by the base class contract to be an error. So I agree that an explicate foo() in{} should be used and that foo() in { assert(0); } looks like an ugly workaround, and would prefer not to restate the inherited class contract.

(In reply to comment #17) > > However, Don's proposal make sense (defining how contract is executed at > > callee's place instead of caller's place). > > Don's proposal is to remove 'in' contract widening completely. That does not > make a lot of sense to me. I did NOT propose that. I merely stated that it's a niche feature, because it only applies when calling a derived function directly, which is unusual behaviour. To restate: If you call any function f, your call MUST satisfy the in contracts of that function. If that function f has inherited a precondition from another function fbase, then the precondition may be weaker than the precondition of fbase. If f happens to ultimately be a call to fderived, with an even weaker precondition, that's irrelevant. You're not allowed to know that, it's an implementation detail -- you called f, not fderived. Only if you call fderived directly, are you allowed to take advantage of fderived's weaker precondition. I think that DMD's precondition widening algorithm may be OK. It can even be OK for fderived to have no in contract. That means, that if you call it *directly*, there are no rules about parameters. But, this should not obviate the callers requirements inherited from fbase. What this means in practice is that in contracts must be BEFORE the vtable lookup, rather than being in the body of the function.

(In reply to comment #22) > (In reply to comment #17) > > > However, Don's proposal make sense (defining how contract is executed at > > > callee's place instead of caller's place). > > > > Don's proposal is to remove 'in' contract widening completely. That does not > > make a lot of sense to me. > > I did NOT propose that. I merely stated that it's a niche feature, because it > only applies when calling a derived function directly, which is unusual > behaviour. > It is not very unusual. It may be infrequent in some systems but it is not unusual. > To restate: > If you call any function f, your call MUST satisfy the in contracts of that > function. If that function f has inherited a precondition from another function > fbase, then the precondition may be weaker than the precondition of fbase. > > If f happens to ultimately be a call to fderived, with an even weaker > precondition, that's irrelevant. You're not allowed to know that, it's an > implementation detail -- you called f, not fderived. Only if you call fderived > directly, are you allowed to take advantage of fderived's weaker precondition. > > I think that DMD's precondition widening algorithm may be OK. It can even be OK > for fderived to have no in contract. Yes, but in that case the existing contract from the overridden method must be inherited. It is quite unusual that a child method has no constraints whatsoever on its input when there were reasons to constrain the valid input to the parent class. > That means, that if you call it > *directly*, there are no rules about parameters. But, this should not obviate > the callers requirements inherited from fbase. That is not what is wanted in practice. > > What this means in practice is that in contracts must be BEFORE the vtable > lookup, rather than being in the body of the function. Yes, that is issue 6857.

(In reply to comment #23) > (In reply to comment #22) > > What this means in practice is that in contracts must be BEFORE the vtable > > lookup, rather than being in the body of the function. > > Yes, that is issue 6857. OK, then this issue is quite simple. All that seems to be required is, to define "no in() contract" to mean "use default precondition". So that if a derived class has no in(), instead of getting base.in() || true (which means that the precondition gets stripped away) it gets base.in() || false. (which means it uses the precondition from the base class). As now, an explicit in{} strips the precondition away. And nothing else needs to change. Works?

Yes, I think that works. The issue can be resolved by making the default 'in' contract empty if the method is introduced without overriding another and 'assert(false)' if the method overrides another.

(In reply to comment #24) > Works? Lovely.

*** Issue 8027 has been marked as a duplicate of this issue. ***

Not sure why this wasn't flagged as INVALID before. But now that the summary line's changed and some comments to the effect of it have been posted, it's essentially an enhancement request. But it'll probably be rejected because the code breakage that would result.

(In reply to comment #28) > But it'll probably be rejected because the code breakage that would result. In several cases breaking some code is the best solution. Is this one of those cases?

(In reply to comment #28) > Not sure why this wasn't flagged as INVALID before. But now that the summary > line's changed and some comments to the effect of it have been posted, it's > essentially an enhancement request. This issue makes the feature basically useless. About half the point of contracts is that they are inherited. The spec contains a bug. This is not a valid implementation of dbc. > But it'll probably be rejected because the code breakage that would result. Code is broken now, without contracts catching it because people do not care about tracking down all methods that override a method that specifies an in-contract and adding an in { assert(0); } contract. It is basically never the case that a overridden method does not need to rely on any in-contract if the super class method does. This is stupid, and everyone actually using the feature will agree with me.

(In reply to comment #28) > Not sure why this wasn't flagged as INVALID before. But now that the summary > line's changed and some comments to the effect of it have been posted, it's > essentially an enhancement request. But it'll probably be rejected because the > code breakage that would result. The line between a fix and an enhancement here is very thin. As other people pointed out, in contract inheritance as they are are not only useless, but extremely dangerous, because they give a false sense of security. Is really hard to debug a problem where you think some preconditions are met (because the code say so), but they really aren't.

(In reply to comment #31) > Is really hard to debug a problem where you think some > preconditions are met (because the code say so), but they really > aren't. But the same applies to such a method in a base class where the override does have an explicit in contract. So if that's a valid reason, then it shouldn't be possible to override in contracts at all. But if we implemented this change, it would lead to confusion and fragility as the legal inputs to a method depend on whether it overrides one with an in contract. Even with issue 3836 done and dusted, it can be annoying to have to walk up the class hierarchy to ascertain what the in contract of a method is, even whether it has a in contract at all. Maybe the right course of action is to _require_ an explicit in contract if the superclass defines one. Since there are alternative ways to remove this (mis)feature, I'm tweaking the summary line.

A weaker precondition B compared to the stronger precondition A is in the mathematical and logical sense an implication: A -> B That means firstly, whenever the precondition A is met then the weaker condition B _must_ be met, too. Also logically this means: not B -> not A. As B has the weaker condition, every time B is not met, A _must_ not be met too. This is because B meets _at least_ all cases that A meets. This is the definition of a weaker condition. Also: interface A { void foo() in { // strong precondition } } class B : A { override void foo() in { // weaker precondition } body { } } A a = new B(); a.foo(); // The precondition of A must be checked. B b = new B(); b.foo(); // The precondition of B must be checked. Also in the above example's call a.foo(), we must use the static type A to determine the precondition. If we would take the precondition of type B in consideration, we would check a too weak precondition. this violates the Liskov substitution principle! In the call b.foo() we must only check the precondition of type B as this is the weaker one. If it succeeds all is fine. If it fails then the precondition of A would fail too, as B covers at least all cases in which of A does not fail (see the implications at the top). Also I recommend to force every derived precondition to enforce the use of a keyword like "weaken" to explicitly show that this must be a weaker precondition: class B : A { override void foo() weaken in { // weaker precondition } body { } }

*** Issue 11835 has been marked as a duplicate of this issue. ***

@ibuclaw updated dlang/dmd pull request #7510 "fix Issue 6856 - Use in contract from base class if not specified in derived" fixing this issue: - fix Issue 6856 - Use in contract from base class if not specified in derived https://github.com/dlang/dmd/pull/7510

*** Issue 12247 has been marked as a duplicate of this issue. ***

THIS ISSUE HAS BEEN MOVED TO GITHUB https://github.com/dlang/dmd/issues/18375 DO NOT COMMENT HERE ANYMORE, NOBODY WILL SEE IT, THIS ISSUE HAS BEEN MOVED TO GITHUB