[Issue 7584] New: contract checking is too conservative for inherited contracts

[d-bugmail at puremagic.com]

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 at puremagic.com
        ReportedBy: timon.gehr at gmx.ch


--- Comment #0 from timon.gehr at 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: -------