www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 7584] New: contract checking is too conservative for inherited contracts

reply d-bugmail puremagic.com writes:
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: -------
Feb 25 2012
next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 26 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 26 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 26 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 26 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 26 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
May 02 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
May 03 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
May 03 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
May 03 2012
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=7584



--- Comment #10 from timon.gehr gmx.ch 2012-05-03 08:53:53 PDT ---
(In reply to comment #9)

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


This seems to be correct. Thank you for looking it up.

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