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

           Summary: contract checking is too conservative for inherited
                    contracts
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD
        AssignedTo: nobody@puremagic.com
        ReportedBy: timon.gehr@gmx.ch


--- Comment #0 from timon.gehr@gmx.ch 2012-02-25 09:12:55 PST ---
Consider the following D program:

class Foo{
    int foo(int x)in{
        assert(x==0);
    }out(result){
        assert(result==0);
    }body{
        return 0;
    }
}
class Bar: Foo{
    override int foo(int x)in{
        assert(x==1); // widen interface
    }out(result){     // specify semantics
        assert(result==x);
    }body{
        return x;     // implementation for wider interface
    }
}

void main(){
    auto bar = new Bar;
    bar.foo(1);
}


Bar clearly is a behavioral subtype of Foo, since Bar.foo does exactly the same thing for the set of acceptable values of Foo.foo. Bar.foo furthermore has a smart implementation the base class cannot possibly be aware of. This is required so that Bar.foo can actually widen the interface and do the right thing for all members of the larger set of input values. Everything is sound.

With DMD 2.058, the program terminates with an assertion failure because it fails the first 'out' contract. This is nonsensical.

Proposed enhancement:
The 'out' contract should only be checked if the corresponding 'in' contract
passes.
(Put differently, the condition that should be checked is that each passing
'in' contract implies the passing of its corresponding 'out' contract. An 'out'
contract does not need to pass if the corresponding 'in' contract fails.)

IIRC, this is how contract inheritance works in Spec#. Spec# is (ahead of) state of the art in this area.

-- 
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=7584


deadalnix <deadalnix@gmail.com> changed:

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


--- Comment #1 from deadalnix <deadalnix@gmail.com> 2012-02-26 04:32:47 PST ---
User of Foo will expect that the output of the function is 0 (as mentionned in the contract). Bar is violating Liskov's substitution principle.

I think you are confusing DbC with unit testing.

-- 
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=7584



--- Comment #2 from timon.gehr@gmx.ch 2012-02-26 05:03:25 PST ---
Again, give an example. Your claim is not true.

-- 
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=7584



--- Comment #3 from deadalnix <deadalnix@gmail.com> 2012-02-26 07:35:07 PST ---
(In reply to comment #2)
> Again, give an example. Your claim is not true.

In Foo, you sated, by contract, that the function must return 0. Any piece of code using an object of type Foo rely on the fact that this function return 0. It is in the contract.

As Bar is a subclass of Foo, it has to respect the contract. An object of type Bar can be passed to any piece of code expecting an object of type Foo. So, that piece of code cannot rely on that contract anymore.

In your case, the out contract of Foo.foo should be an unittest. You want that to be true for object of type Foo, but not for object of subtypes. So contract isn't the right tool for the job.

Bar doesn't respect Foo's contract, so the contract must fail. This is the expected behavior. If it weren't the case, then it would be a violation of Liskov substitution principle, because I couldn't pass an object of type Bar to a piece of code expecting Foo.

-- 
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=7584



--- Comment #4 from timon.gehr@gmx.ch 2012-02-26 08:17:35 PST ---
LSP is not violated. That is the point. The rules proposed here are sufficient to guarantee LSP. The rules that are currently employed are too conservative. Think about it.

void main(){
    Foo foo = new Bar;
    foo.foo(0); // call ok, returns 0
    // foo.foo(1); // _call_ not ok, violates in contract
}

Also see issue 6857.

-- 
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=7584



--- Comment #5 from deadalnix <deadalnix@gmail.com> 2012-02-26 08:28:57 PST ---
(In reply to comment #4)
> LSP is not violated. That is the point. The rules proposed here are sufficient to guarantee LSP. The rules that are currently employed are too conservative. Think about it.
> 
> void main(){
>     Foo foo = new Bar;
>     foo.foo(0); // call ok, returns 0
>     // foo.foo(1); // _call_ not ok, violates in contract
> }
> 
> Also see issue 6857.

issue 6857 is a valid point. I just did a post about that on the newsgroup.

It means, in the proposed example, that the in contract should fail. So the out contract never reached.

You definitively have a point here.

-- 
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=7584


Walter Bright <bugzilla@digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
                 CC|                            |bugzilla@digitalmars.com
         Resolution|                            |INVALID


--- Comment #6 from Walter Bright <bugzilla@digitalmars.com> 2012-05-02 18:13:18 PDT ---
Out contracts are "anded" together, meaning that *all* out contracts must pass in an inheritance hierarchy. Out contracts in overriding functions do not override the out contract in the overridden function, nor are they at all associated with any in contracts.

-- 
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=7584



--- Comment #7 from timon.gehr@gmx.ch 2012-05-03 02:20:30 PDT ---
(In reply to comment #6)
> Out contracts are "anded" together, meaning that *all* out contracts must pass in an inheritance hierarchy. Out contracts in overriding functions do not override the out contract in the overridden function, nor are they at all associated with any in contracts.

The point here was that they should be. Why should the method work hard to satisfy the postcondition, if the caller fails to satisfy the corresponding precondition?

-- 
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=7584



--- Comment #8 from deadalnix <deadalnix@gmail.com> 2012-05-03 04:18:22 PDT ---
(In reply to comment #6)
> Out contracts are "anded" together, meaning that *all* out contracts must pass in an inheritance hierarchy. Out contracts in overriding functions do not override the out contract in the overridden function, nor are they at all associated with any in contracts.

What you have here is, in fact, over restrictive to ensure OOP expectations.

With both your proposal and Timon's D is fine in regard of OOP.

Now, Timon's proposal does allow more than the current behavior (and still allow the current behavior). You have to see it as a generalization of an over restrictive solution.

-- 
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=7584


Andrei Alexandrescu <andrei@metalanguage.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |andrei@metalanguage.com


--- Comment #9 from Andrei Alexandrescu <andrei@metalanguage.com> 2012-05-03 07:44:53 PDT ---
(In reply to comment #0)
> IIRC, this is how contract inheritance works in Spec#. Spec# is (ahead of) state of the art in this area.

According to my reading of http://http://research.microsoft.com/en-us/um/people/leino/papers/krml136.pdf, page 9, paragraph 1, Spec# does not allow overriding of preconditions so it can't be used here as an example.

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