http://d.puremagic.com/issues/show_bug.cgi?id=6857

           Summary: Precondition contract checks should be statically
                    bound.
           Product: D
           Version: D2
          Platform: Other
        OS/Version: All
            Status: NEW
          Severity: normal
          Priority: P2
         Component: DMD
        AssignedTo: nobody@puremagic.com
        ReportedBy: timon.gehr@gmx.ch


--- Comment #0 from timon.gehr@gmx.ch 2011-10-26 14:08:40 PDT ---
import std.stdio;

class A{
    void foo()in{writeln("A, in!");assert(false);}out{writeln("A,
out!");}body{}
}
class B:A{
    override void foo()in{writeln("B, in!");}out{writeln("B, out!");}body{}
}

void main(){
    A x = new B;
    x.foo(); // prints all four messages
}

It is an error for the caller of foo to rely on the widened interface of B, because the static type of x is A. Therefore only the in-contract of A should be checked. The way it is now, in contracts provide no means of reasoning about the validity of the code if the dynamic type of some instance is unknown during compilation.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


jens.k.mueller@gmx.de changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |jens.k.mueller@gmx.de


--- Comment #1 from jens.k.mueller@gmx.de 2012-03-01 07:22:17 PST ---
Can you elaborate why the static type must be considered? What's the problem with using the dynamic type?

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


deadalnix <deadalnix@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |deadalnix@gmail.com


--- Comment #2 from deadalnix <deadalnix@gmail.com> 2012-03-01 07:40:10 PST ---
(In reply to comment #1)
> Can you elaborate why the static type must be considered? What's the problem with using the dynamic type?

The problem is simple. Let's consider a class A and a subclass B.

Then a function as this :

void fun(A a) {
    a.foo();
}

If passed an element of type B, fun will work, because B is a subclass of A. If B.foo's contract is different than A.foo's, then B.foo's in contract is executed.

It is a bug, because fun has no knowledge weither it manipulate an element of type A or an element of type B. It means that fun must respect the in contract provided by A.foo, because in other case, it may or may no work, depending on how fun in called, which isn't a reliable behavior.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857



--- Comment #3 from jens.k.mueller@gmx.de 2012-03-02 00:35:52 PST ---
(In reply to comment #2)
> (In reply to comment #1)
> > Can you elaborate why the static type must be considered? What's the problem with using the dynamic type?
> 
> The problem is simple. Let's consider a class A and a subclass B.
> 
> Then a function as this :
> 
> void fun(A a) {
>     a.foo();
> }
> 
> If passed an element of type B, fun will work, because B is a subclass of A. If B.foo's contract is different than A.foo's, then B.foo's in contract is executed.
> 
> It is a bug, because fun has no knowledge weither it manipulate an element of type A or an element of type B. It means that fun must respect the in contract provided by A.foo, because in other case, it may or may no work, depending on how fun in called, which isn't a reliable behavior.

Yesterday I was sleepy and wasn't able to understand it. But even now I fail to
see the issue.
First fun accepts any instance that is of class A or a subclass of A. And
independent of this whenever you call a.foo() all in contracts must be checked
using based on a's dynamic type.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


Don <clugdbug@yahoo.com.au> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |clugdbug@yahoo.com.au


--- Comment #4 from Don <clugdbug@yahoo.com.au> 2012-03-02 01:57:16 PST ---
(In reply to comment #3)
> (In reply to comment #2)
> > (In reply to comment #1)
> > > Can you elaborate why the static type must be considered? What's the problem with using the dynamic type?
> > 
> > The problem is simple. Let's consider a class A and a subclass B.
> > 
> > Then a function as this :
> > 
> > void fun(A a) {
> >     a.foo();
> > }
> > 
> > If passed an element of type B, fun will work, because B is a subclass of A. If B.foo's contract is different than A.foo's, then B.foo's in contract is executed.
> > 
> > It is a bug, because fun has no knowledge weither it manipulate an element of type A or an element of type B. It means that fun must respect the in contract provided by A.foo, because in other case, it may or may no work, depending on how fun in called, which isn't a reliable behavior.
> 
> Yesterday I was sleepy and wasn't able to understand it. But even now I fail to
> see the issue.
> First fun accepts any instance that is of class A or a subclass of A. And
> independent of this whenever you call a.foo() all in contracts must be checked
> using based on a's dynamic type.

The point is that fun() must satisfy the precondition for A. The fact that it's
actually receiving a subclass of A is irrelevant.
Since subclasses of A can only widen the precondition, they don't need to be
checked. (Since they must pass A.in(), by definition they will pass A.in() ||
B.in()).

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


timon.gehr@gmx.ch changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|RESOLVED                    |REOPENED
         Resolution|INVALID                     |
           Severity|normal                      |enhancement


--- Comment #6 from timon.gehr@gmx.ch 2012-05-02 13:14:21 PDT ---
(In reply to comment #5)
> This report is invalid,

I disagree.

> it is working as designed.
> 

Therefore the design is flawed and this report is an enhancement.

> This is how inheritance of contracts and overriding of functions is supposed to work.
> 

This report is not about how inheritance and overriding work, it is about static vs. dynamic binding. (Though inheritance and overriding of contracts also don't work how they are supposed to work, see issues 6856 and 7584.)

> >void fun(A a)
> >The point is that fun() must satisfy the precondition for A.
> 
> This is incorrect. It must satisfy the precondition for A or any class derived from A.

How does it know which one to satisfy? If it does, it might as well just downcast the reference in order to get a wider interface. If it does not, it is a bug in fun() if it fails to satisfy the precondition for A. (It's signature claims it can handle all A's!)

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


Walter Bright <bugzilla@digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|REOPENED                    |RESOLVED
         Resolution|                            |INVALID


--- Comment #7 from Walter Bright <bugzilla@digitalmars.com> 2012-05-02 14:11:46 PDT ---
This is a misunderstanding about how inheritance works. If an A is passed to foo(), then only A's preconditions are checked. If a B is passed, then either A's precondition or B's precondition must be satisified.

This is how standard inheritance works. I did not invent this.

It is not a bug, and changing this behavior would completely break how inheritance works.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


timon.gehr@gmx.ch changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
         Resolution|INVALID                     |WONTFIX


--- Comment #8 from timon.gehr@gmx.ch 2012-05-02 15:10:01 PDT ---
(In reply to comment #7)
> This is a misunderstanding about how inheritance works.

No, it is not. The precondition is what needs to be satisfied by the client of the method. The client has no way to know what exactly to satisfy if the precondition is dynamically bound, therefore the client usually has to assume that they have to satisfy the statically bound precondition. Failure to do so is a bug most of the time.

I am not going to argue this further. It can probably go either way. The current behavior detects less bugs, but the proposed change would make writing contracts for certain cases cases where eg. a method accepts a parameter that has distinct restrictions depending on the result of a previous method invocation on the same object a little bit harder.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857



--- Comment #10 from Walter Bright <bugzilla@digitalmars.com> 2012-05-02 16:27:15 PDT ---
I suggest checking Bertrand Meyer's book Object-Oriented Software Construction, which is the definitive reference on this. It's theoretically sound. I did not invent the design, I implemented it.

The fundamental nature of 'in' contracts is that they are "loosened" on derivation. If an instance of B is passed to parameter A, then if either the contract for A or the contract for B passes, then it passes. It is NOT necessary for the A contract to pass. This is exactly what you're seeing in the example.

If an instance of A is passed, then the contract for A must pass.

It isn't a bug, it is the way it is supposed to work. Nor am I ignoring it - I'm trying to explain it.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=6857


Andrei Alexandrescu <andrei@metalanguage.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |andrei@metalanguage.com
         Resolution|WONTFIX                     |INVALID


--- Comment #11 from Andrei Alexandrescu <andrei@metalanguage.com> 2012-05-02 16:40:01 PDT ---
>The current specification is flawed. It have nothing to do with how inheritance work (and I could assure you I know what I'm talking about, and I'm also pretty sure Timon knows also).

Mistakes happen to the best of us. In this case the specification is correct and the bug report is in error. Derived classes may require less and provide more, which in contract lingo translates into weaker "in" contracts and stronger "out" contracts. This is not a matter in which reasonable people may disagree and not a matter of opinion.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------