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: nob...@puremagic.com
ReportedBy: timon.g...@gmx.ch
--- Comment #0 from timon.g...@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: -------
