www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - define in contract according to the caller, not the callee.

reply deadalnix <deadalnix gmail.com> writes:
Everything start from this bug report : 
http://d.puremagic.com/issues/show_bug.cgi?id=6856

And the piece of code associated :

import std.stdio;

class A{
     void foo()in{writeln("in!");}out{writeln("out!");}body{}
}
class B:A{
     override void foo(){} // add in{assert(false);}body to get it working
}

void main(){
     A x = new A;
     x.foo(); // in! \ out!
     B y = new B;
     y.foo(); // out!
}

B.foo in contract isn't specified, so it is implicitly deduced that no 
preconditions have to be checked. As B.foo preconditions are always 
respected, A.foo precondition is never called on object of type B.

Now, let consider this function :

void fun(A a) {
     a.foo();
}

We can call fun with parameters of type A and B, because B is a subclass 
of A. If we call fun with a parameter of type B, then A.foo's 
precondition are not checked. This is a problem, because fun isn't 
supposed to know that it manipulate an object of type B, so should 
respect A.foo's preconditions. In fact, if fun call foo in a way that 
respect B.foo's precondition, but not A.foo's, it must be considered as 
an issue, because fun isn't supposed to know that it manipulate an 
object of type B.

Precondition are supposed to be respected by the caller, as opposed to 
postconditions. So the checked contract must be selected according to 
the type at caller's place, not callee's place.

In this regard, the bug report quoted here should be marked as invalid, 
but another open, with the restated issue. Or am I wrong ?
Feb 26 2012
next sibling parent deadalnix <deadalnix gmail.com> writes:
And the bug report : http://d.puremagic.com/issues/show_bug.cgi?id=6857

Le 26/02/2012 17:26, deadalnix a écrit :
 Everything start from this bug report :
 http://d.puremagic.com/issues/show_bug.cgi?id=6856

 And the piece of code associated :

 import std.stdio;

 class A{
 void foo()in{writeln("in!");}out{writeln("out!");}body{}
 }
 class B:A{
 override void foo(){} // add in{assert(false);}body to get it working
 }

 void main(){
 A x = new A;
 x.foo(); // in! \ out!
 B y = new B;
 y.foo(); // out!
 }

 B.foo in contract isn't specified, so it is implicitly deduced that no
 preconditions have to be checked. As B.foo preconditions are always
 respected, A.foo precondition is never called on object of type B.

 Now, let consider this function :

 void fun(A a) {
 a.foo();
 }

 We can call fun with parameters of type A and B, because B is a subclass
 of A. If we call fun with a parameter of type B, then A.foo's
 precondition are not checked. This is a problem, because fun isn't
 supposed to know that it manipulate an object of type B, so should
 respect A.foo's preconditions. In fact, if fun call foo in a way that
 respect B.foo's precondition, but not A.foo's, it must be considered as
 an issue, because fun isn't supposed to know that it manipulate an
 object of type B.

 Precondition are supposed to be respected by the caller, as opposed to
 postconditions. So the checked contract must be selected according to
 the type at caller's place, not callee's place.

 In this regard, the bug report quoted here should be marked as invalid,
 but another open, with the restated issue. Or am I wrong ?

Feb 26 2012
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 02/26/2012 05:26 PM, deadalnix wrote:
 Everything start from this bug report :
 http://d.puremagic.com/issues/show_bug.cgi?id=6856

 And the piece of code associated :

 import std.stdio;

 class A{
 void foo()in{writeln("in!");}out{writeln("out!");}body{}
 }
 class B:A{
 override void foo(){} // add in{assert(false);}body to get it working
 }

 void main(){
 A x = new A;
 x.foo(); // in! \ out!
 B y = new B;
 y.foo(); // out!
 }

 B.foo in contract isn't specified, so it is implicitly deduced that no
 preconditions have to be checked.

That is the wrong way to go about it. When would you want that? Removing the in-contract must be explicit. (in{}) Otherwise, the whole concept of contract inheritance is implemented in a bogus way. (The absence of a contract would be able to override the presence of another one and silence contract violations that might indicate serious bugs in the software.)
 As B.foo preconditions are always
 respected, A.foo precondition is never called on object of type B.

 Now, let consider this function :

 void fun(A a) {
 a.foo();
 }

 We can call fun with parameters of type A and B, because B is a subclass
 of A. If we call fun with a parameter of type B, then A.foo's
 precondition are not checked. This is a problem, because fun isn't
 supposed to know that it manipulate an object of type B, so should
 respect A.foo's preconditions. In fact, if fun call foo in a way that
 respect B.foo's precondition, but not A.foo's, it must be considered as
 an issue, because fun isn't supposed to know that it manipulate an
 object of type B.

 Precondition are supposed to be respected by the caller, as opposed to
 postconditions. So the checked contract must be selected according to
 the type at caller's place, not callee's place.

Exactly.
 In this regard, the bug report quoted here should be marked as invalid,
 but another open, with the restated issue. Or am I wrong ?

Yes.
Feb 26 2012
parent deadalnix <deadalnix gmail.com> writes:
Le 26/02/2012 17:40, Timon Gehr a écrit :
 On 02/26/2012 05:26 PM, deadalnix wrote:
 Everything start from this bug report :
 http://d.puremagic.com/issues/show_bug.cgi?id=6856

 And the piece of code associated :

 import std.stdio;

 class A{
 void foo()in{writeln("in!");}out{writeln("out!");}body{}
 }
 class B:A{
 override void foo(){} // add in{assert(false);}body to get it working
 }

 void main(){
 A x = new A;
 x.foo(); // in! \ out!
 B y = new B;
 y.foo(); // out!
 }

 B.foo in contract isn't specified, so it is implicitly deduced that no
 preconditions have to be checked.

That is the wrong way to go about it. When would you want that? Removing the in-contract must be explicit. (in{}) Otherwise, the whole concept of contract inheritance is implemented in a bogus way. (The absence of a contract would be able to override the presence of another one and silence contract violations that might indicate serious bugs in the software.)

Using caller's place type to determine what is the in contract would really improve things on this problem. All polymorphic uses of the type would still have to respect the contract. Requiring an explicit "in {}" is something we should consider.
Feb 26 2012