Summary: contract checking is too conservative for inherited
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD

--- Comment #0 from 2012-02-25 09:12:55 PST ---
Consider the following D program:

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

void main(){
    auto bar = new Bar;;

Bar clearly is a behavioral subtype of Foo, since does exactly the same
thing for the set of acceptable values of furthermore has a
smart implementation the base class cannot possibly be aware of. This is
required so that 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
(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:
------- You are receiving this mail because: -------

Reply via email to