www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Shortcut evaluation for hierarchy of in contracts

reply Jens Mueller <jens.k.mueller gmx.de> writes:
Hi,

a student of our seminar observed a questionable behavior when checking
in contracts/pre conditions in a polymorphic hierarchy.
When checking in contracts for polymorphic classes they are verified
starting at the base class but with shortcuts. I.e. the first in
contract that works causes to skip executing of following contracts.
This is perfectly valid because in contracts are only allowed to
require less. But what if the programmer fails to follow this rule? Why
not checking all in contracts. Since contracts are compiled out in
release mode I argue it's worth the extra cycles to detect some
inconsistency in the contracts. Polymorphic hierarchies can be deep.
Consider the following example

check_require_less.d:
unittest {
    class Base {
        void foo(uint i)
            in { assert(i <= 10); }
        body { }
    }
    
    class Sub : Base {   
        override void foo(uint i)
            in { assert(i <= 5); } // fails to require less but I won't know
        body
        {
            assert(i <= 5); // fails here because in contract wasn't checked
        }
    }
    
    auto s = new Sub;
    //s.foo(10); // fails as expected
    s.foo(7); // due to shortcut evaluation of in contracts this call passes
all contracts
}

$ rdmd --main -unittest check_require_less.d

In the case above s.foo(7) will fail but this is only due to the fact
that I recheck the contract. If I wouldn't s.foo() may be executed and
the programmer assumes that i <= 5 holds. Thus, s.foo() gets executed
based on wrong assumptions. Hence, s.foo() may not work properly. A fact
that is hidden from the programmer.

Jens
Jun 30 2011
parent reply bearophile <bearophileHUGS lycos.com> writes:
Jens Mueller:


 unittest {
     class Base {
         void foo(uint i)
             in { assert(i <= 10); }
         body { }
     }
     
     class Sub : Base {   
         override void foo(uint i)
             in { assert(i <= 5); } // fails to require less but I won't know
         body
         {
             assert(i <= 5); // fails here because in contract wasn't checked
         }
     }
     
     auto s = new Sub;
     //s.foo(10); // fails as expected
     s.foo(7); // due to shortcut evaluation of in contracts this call passes
all contracts
 }


I think it's a DMD bug, fit for Bugzilla if not already present.

Bye,
bearophile
Jun 30 2011
parent reply Jens Mueller <jens.k.mueller gmx.de> writes:
bearophile wrote:

 Jens Mueller:
 

 unittest {
     class Base {
         void foo(uint i)
             in { assert(i <= 10); }
         body { }
     }
     
     class Sub : Base {   
         override void foo(uint i)
             in { assert(i <= 5); } // fails to require less but I won't know
         body
         {
             assert(i <= 5); // fails here because in contract wasn't checked
         }
     }
     
     auto s = new Sub;
     //s.foo(10); // fails as expected
     s.foo(7); // due to shortcut evaluation of in contracts this call passes
all contracts
 }


 
 I think it's a DMD bug, fit for Bugzilla if not already present.


The shortcut evaluation is specified in TDPL. That's why I assume the
behavior is intended.

Jens
Jun 30 2011
next sibling parent reply "Robert Jacques" <sandford jhu.edu> writes:
On Thu, 30 Jun 2011 06:42:57 -0400, Jens Mueller <jens.k.mueller gmx.de>  
wrote:


 bearophile wrote:

 Jens Mueller:


 unittest {
     class Base {
         void foo(uint i)
             in { assert(i <= 10); }
         body { }
     }

     class Sub : Base {
         override void foo(uint i)
             in { assert(i <= 5); } // fails to require less but I  


 won't know

         body
         {
             assert(i <= 5); // fails here because in contract wasn't  


 checked

         }
     }

     auto s = new Sub;
     //s.foo(10); // fails as expected
     s.foo(7); // due to shortcut evaluation of in contracts this call  


 passes all contracts

 }


 I think it's a DMD bug, fit for Bugzilla if not already present.


 The shortcut evaluation is specified in TDPL. That's why I assume the
 behavior is intended.

 Jens


A subclass must be able to handle all the inputs the base class accepts,  
otherwise it isn't true polymorphism anymore. Not being able to use Sub  
where Base is expected, and maybe only Base was tested, can lead to major  
bugs.
Jun 30 2011
parent reply Jens Mueller <jens.k.mueller gmx.de> writes:
Robert Jacques wrote:

 On Thu, 30 Jun 2011 06:42:57 -0400, Jens Mueller
 <jens.k.mueller gmx.de> wrote:
 

bearophile wrote:

Jens Mueller:


 unittest {
     class Base {
         void foo(uint i)
             in { assert(i <= 10); }
         body { }
     }

     class Sub : Base {
         override void foo(uint i)
             in { assert(i <= 5); } // fails to require less


but I won't know

         body
         {
             assert(i <= 5); // fails here because in contract


wasn't checked

         }
     }

     auto s = new Sub;
     //s.foo(10); // fails as expected
     s.foo(7); // due to shortcut evaluation of in contracts


this call passes all contracts

 }


I think it's a DMD bug, fit for Bugzilla if not already present.


The shortcut evaluation is specified in TDPL. That's why I assume the
behavior is intended.

Jens


 
 A subclass must be able to handle all the inputs the base class
 accepts, otherwise it isn't true polymorphism anymore. Not being
 able to use Sub where Base is expected, and maybe only Base was
 tested, can lead to major bugs.


So you agree that the current behavior is error-prone?

Jens
Jun 30 2011
parent reply "Robert Jacques" <sandford jhu.edu> writes:
On Fri, 01 Jul 2011 02:39:29 -0400, Jens Mueller <jens.k.mueller gmx.de>  
wrote:

 Robert Jacques wrote:

 On Thu, 30 Jun 2011 06:42:57 -0400, Jens Mueller
 <jens.k.mueller gmx.de> wrote:


bearophile wrote:

Jens Mueller:


 unittest {
     class Base {
         void foo(uint i)
             in { assert(i <= 10); }
         body { }
     }

     class Sub : Base {
         override void foo(uint i)
             in { assert(i <= 5); } // fails to require less


but I won't know

         body
         {
             assert(i <= 5); // fails here because in contract


wasn't checked

         }
     }

     auto s = new Sub;
     //s.foo(10); // fails as expected
     s.foo(7); // due to shortcut evaluation of in contracts


this call passes all contracts

 }


I think it's a DMD bug, fit for Bugzilla if not already present.


The shortcut evaluation is specified in TDPL. That's why I assume the
behavior is intended.

Jens


 A subclass must be able to handle all the inputs the base class
 accepts, otherwise it isn't true polymorphism anymore. Not being
 able to use Sub where Base is expected, and maybe only Base was
 tested, can lead to major bugs.


 So you agree that the current behavior is error-prone?


No. I think the current behavior is correct. In fact, if anything, D  
shouldn't allow you to define an in contract on any override method. A Sub  
is a Base and therefore must be able to handle all inputs that are valid  
for a Base.
Jul 01 2011
next sibling parent simendsjo <simendsjo gmail.com> writes:
On 02.07.2011 01:32, Robert Jacques wrote:

 On Fri, 01 Jul 2011 02:39:29 -0400, Jens Mueller <jens.k.mueller gmx.de>
 wrote:

 Robert Jacques wrote:

 On Thu, 30 Jun 2011 06:42:57 -0400, Jens Mueller
 <jens.k.mueller gmx.de> wrote:


bearophile wrote:

Jens Mueller:


 unittest {
 class Base {
 void foo(uint i)
 in { assert(i <= 10); }
 body { }
 }

 class Sub : Base {
 override void foo(uint i)
 in { assert(i <= 5); } // fails to require less


but I won't know

 body
 {
 assert(i <= 5); // fails here because in contract


wasn't checked

 }
 }

 auto s = new Sub;
 //s.foo(10); // fails as expected
 s.foo(7); // due to shortcut evaluation of in contracts


this call passes all contracts

 }


I think it's a DMD bug, fit for Bugzilla if not already present.


The shortcut evaluation is specified in TDPL. That's why I assume the
behavior is intended.

Jens


 A subclass must be able to handle all the inputs the base class
 accepts, otherwise it isn't true polymorphism anymore. Not being
 able to use Sub where Base is expected, and maybe only Base was
 tested, can lead to major bugs.


 So you agree that the current behavior is error-prone?


 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


Have to agree. By tightening the contracts in subclasses, you'll break 
Liskov substitution principle.
Jul 01 2011
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 7/1/11 6:32 PM, Robert Jacques wrote:

 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


That is a sensible enhancement.

Andrei
Jul 02 2011
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Andrei Alexandrescu wrote:

 On 7/1/11 6:32 PM, Robert Jacques wrote:

 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


 That is a sensible enhancement.

 Andrei


How so? The child class should still be able to take more general inputs than
the
parent: by specifying an in contract on an override method.
How would you reach that goal otherwise?

Timon
Jul 02 2011
parent reply David Nadlinger <see klickverbot.at> writes:
On 7/3/11 1:16 AM, Timon Gehr wrote:

 Andrei Alexandrescu wrote:

 On 7/1/11 6:32 PM, Robert Jacques wrote:

 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


 That is a sensible enhancement.

 Andrei


 How so? The child class should still be able to take more general inputs than
the
 parent: by specifying an in contract on an override method.
 How would you reach that goal otherwise?

 Timon


In any case, I consider the current implementation buggy, as having no 
in contract in the superclass is different from having an empty in 
contract there:

---
class Foo {
   void baz(int i) {}
}

class Bar : Foo {
   override void baz(int i) in {
     assert(i < 5, "I am triggered, but should not be.");
   } body {
     assert(i < 5, "I should be triggered instead of the contract.");
   }
}

void main() {
   auto bar = new Bar;
   bar.baz(6);
}
---

David
Jul 02 2011
parent "Daniel Murphy" <yebblies nospamgmail.com> writes:
"David Nadlinger" <see klickverbot.at> wrote in message 
news:iuodav$2n7s$1 digitalmars.com...

 In any case, I consider the current implementation buggy, as having no in 
 contract in the superclass is different from having an empty in contract 
 there:

 ---
 class Foo {
   void baz(int i) {}
 }

 class Bar : Foo {
   override void baz(int i) in {
     assert(i < 5, "I am triggered, but should not be.");
   } body {
     assert(i < 5, "I should be triggered instead of the contract.");
   }
 }

 void main() {
   auto bar = new Bar;
   bar.baz(6);
 }
 ---

 David


There's a patch for this!
Jul 02 2011
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 7/2/2011 4:04 PM, Andrei Alexandrescu wrote:

 On 7/1/11 6:32 PM, Robert Jacques wrote:

 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


 That is a sensible enhancement.


This would throw out the whole idea of 'loosening'.
Jul 02 2011
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 7/2/11 8:02 PM, Walter Bright wrote:

 On 7/2/2011 4:04 PM, Andrei Alexandrescu wrote:

 On 7/1/11 6:32 PM, Robert Jacques wrote:

 No. I think the current behavior is correct. In fact, if anything, D
 shouldn't allow you to define an in contract on any override method. A
 Sub is a Base and therefore must be able to handle all inputs that are
 valid for a Base.


 That is a sensible enhancement.


 This would throw out the whole idea of 'loosening'.


I mean disallow an override to add an "in" contract where the overridden 
method had a body but no "in" contract.

Andrei
Jul 02 2011
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 7/2/2011 6:56 PM, Andrei Alexandrescu wrote:

 I mean disallow an override to add an "in" contract where the overridden method
 had a body but no "in" contract.


Ok, that makes sense.
Jul 02 2011
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 7/2/11 9:41 PM, Walter Bright wrote:

 On 7/2/2011 6:56 PM, Andrei Alexandrescu wrote:

 I mean disallow an override to add an "in" contract where the
 overridden method
 had a body but no "in" contract.


 Ok, that makes sense.


I hereby am making a request for a pull request.

Andrei
Jul 02 2011
parent reply "Daniel Murphy" <yebblies nospamgmail.com> writes:
"Andrei Alexandrescu" <SeeWebsiteForEmail erdani.org> wrote in message 
news:iuonck$586$1 digitalmars.com...

 I hereby am making a request for a pull request.

 Andrei


I'll do it if you make a bug report for it.

Should empty in contracts be treated the same?
Jul 02 2011
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 7/2/11 10:35 PM, Daniel Murphy wrote:

 "Andrei Alexandrescu"<SeeWebsiteForEmail erdani.org>  wrote in message
 news:iuonck$586$1 digitalmars.com...

 I hereby am making a request for a pull request.

 Andrei


 I'll do it if you make a bug report for it.


http://d.puremagic.com/issues/show_bug.cgi?id=6242


 Should empty in contracts be treated the same?


No. They should be the workaround.


Andrei
Jul 02 2011
parent "Daniel Murphy" <yebblies nospamgmail.com> writes:
"Andrei Alexandrescu" <SeeWebsiteForEmail erdani.org> wrote in message 
news:iuorep$bn2$1 digitalmars.com...

 http://d.puremagic.com/issues/show_bug.cgi?id=6242


What should the error message be?
Jul 02 2011
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 6/30/2011 3:42 AM, Jens Mueller wrote:

 The shortcut evaluation is specified in TDPL. That's why I assume the
 behavior is intended.


The behavior is both intended and crucial to the notion of contract inheritance.

The 'in' contract must pass at least one of the 'in' contracts of its 
inheritance hierarchy.
Derived functions "loosen" the requirements for input.

The 'out' contract must pass all of the 'out' contracts.
Derived functions "tighten" the requirements for output.
Jul 01 2011
next sibling parent reply Jens Mueller <jens.k.mueller gmx.de> writes:
Walter Bright wrote:

 On 6/30/2011 3:42 AM, Jens Mueller wrote:

The shortcut evaluation is specified in TDPL. That's why I assume the
behavior is intended.


 
 The behavior is both intended and crucial to the notion of contract
inheritance.
 
 The 'in' contract must pass at least one of the 'in' contracts of
 its inheritance hierarchy.
 Derived functions "loosen" the requirements for input.


Yes. But the problem with passing only one of the in contracts is that
it is error-prone because it *assumes* that for in contracts the
requirements are widened. But what if the programmer fails at loosening
a derived in contract, i.e. he restricted it. In the current setting the
programmer won't know that he did an error. And with deep inheritance
hierarchies it gets more complicated to have all the contracts of super
classes in mind.
Why not check all in contracts to make sure that they follow the
loosening rule? Why not enforce the loosing rule?

Jens
Jul 01 2011
parent Walter Bright <newshound2 digitalmars.com> writes:
On 7/1/2011 1:10 AM, Jens Mueller wrote:

 Yes. But the problem with passing only one of the in contracts is that
 it is error-prone because it *assumes* that for in contracts the
 requirements are widened. But what if the programmer fails at loosening
 a derived in contract, i.e. he restricted it. In the current setting the
 programmer won't know that he did an error. And with deep inheritance
 hierarchies it gets more complicated to have all the contracts of super
 classes in mind.
 Why not check all in contracts to make sure that they follow the
 loosening rule? Why not enforce the loosing rule?


The loosening rule is that one of the in contracts must pass. That's exactly 
what it does. As soon as one passes, there is no need to check the rest.
Jul 01 2011
prev sibling parent reply "Daniel Murphy" <yebblies nospamgmail.com> writes:
"Walter Bright" <newshound2 digitalmars.com> wrote in message 
news:iuju03$27ip$1 digitalmars.com...

 The 'in' contract must pass at least one of the 'in' contracts of its 
 inheritance hierarchy.
 Derived functions "loosen" the requirements for input.


This might be the recommended way to do it, but this is not enforced by the 
compiler, just assumed.

To enforce this, the compiler should give an error if a base function's 
precondition passes but a derived precondition does not.

The requirement is not really that any 'in' contract passing is good enough, 
it's just assumed that all preconditions on inherited functions will pass if 
the base contract does.
Jul 01 2011
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Daniel Murphy wrote:

 "Walter Bright" <newshound2 digitalmars.com> wrote in message
 news:iuju03$27ip$1 digitalmars.com...

 The 'in' contract must pass at least one of the 'in' contracts of its
 inheritance hierarchy.
 Derived functions "loosen" the requirements for input.


 This might be the recommended way to do it, but this is not enforced by the
 compiler, just assumed.

 To enforce this, the compiler should give an error if a base function's
 precondition passes but a derived precondition does not.

 The requirement is not really that any 'in' contract passing is good enough,
 it's just assumed that all preconditions on inherited functions will pass if
 the base contract does.


Actually that is not true. One passing contract is enough. The current (and
correct) behavior enforces that when the parents contract passes, the child's
contract passes too.

If both had to pass, a child class could actually make contracts more
restrictive.
It is this what we want to avoid, right?

The mistake is to assume, that the in contract of the child classes method
consists of what is written there only.
But arguably that is a problem with the language. Compare CP in D to Bertrand
Meyer's DBC in Eiffel:

//D
class Foo{
  void bar(int a, int)
  in{assert(a>0);} // require that a>0
  out(r){assert r>0;}
  body{
    return a;
  }
}

class Qux : Foo{
  override void bar(int a,int b)loosen
  in{assert(b>0);} //'if parents contract fails, I can still produce sensible
behavior if b>0 holds'
  body{
    return a>0?a:b;
  }
}

--Eiffel
class Foo
feature
  bar(a,b:INTEGER)
    require
      a_positive: a>0
    do
      Result:=a
    ensure
      result_positive: Result>0
    end
end

class Qux
inherit
  Foo
    redefine bar end
feature
  bar(a,b:INTEGER)
    require else    -- important!
      b_positive: b>0
    do
      if a>0 then Result:=a
      else Result:=b
    end
end

As you can see, in Eiffel, contract extension has a different syntax than
contract
definition. ('require else' vs. require) In D the syntax is identical, even
though
the two things done are quite different. What effectively is done depends on
whether or not the override keyword is present. I assume it is this that has led
to the misunderstanding.

Now, sure, if the parents contract is

in{assert(a<=10);}

and the child's contract is

in{assert(a<=5);}

then that is almost certainly an error because the child's contract fails to
loosen any restrictions.
But to catch this in the general case, the compiler would have to incorporate a
theorem prover.
(And validity of D code would start to depend on the quality of the theorem
prover
of the respective D compiler ;))

Cheers,
-Timon
Jul 01 2011
parent reply "Daniel Murphy" <yebblies nospamgmail.com> writes:
I don't disagree that tightening contracts for derived functions is a bad 
idea.
I didn't mean the contract should fail, I meant that the program should fail 
with an error that the contract is invalid.

"Timon Gehr" <timon.gehr gmx.ch> wrote in message 
news:iuklvm$pks$1 digitalmars.com...

 Now, sure, if the parents contract is

 in{assert(a<=10);}

 and the child's contract is

 in{assert(a<=5);}

 then that is almost certainly an error because the child's contract fails 
 to
 loosen any restrictions.
 But to catch this in the general case, the compiler would have to 
 incorporate a
 theorem prover.
 (And validity of D code would start to depend on the quality of the 
 theorem prover
 of the respective D compiler ;))


This can be caught at runtime without a theorem prover. (And I think it 
should be)
Jul 01 2011
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Daniel Murphy wrote:

 I don't disagree that tightening contracts for derived functions is a bad
 idea.
 I didn't mean the contract should fail, I meant that the program should fail
 with an error that the contract is invalid.

 "Timon Gehr" <timon.gehr gmx.ch> wrote in message
 news:iuklvm$pks$1 digitalmars.com...

 Now, sure, if the parents contract is

 in{assert(a<=10);}

 and the child's contract is

 in{assert(a<=5);}

 then that is almost certainly an error because the child's contract fails
 to
 loosen any restrictions.
 But to catch this in the general case, the compiler would have to
 incorporate a
 theorem prover.
 (And validity of D code would start to depend on the quality of the
 theorem prover
 of the respective D compiler ;))


 This can be caught at runtime without a theorem prover. (And I think it
 should be)


How would you catch it? I am sure it cannot be caught trivially:

There are 4 possibilities:
1. Both parent and child contract would pass.
2. Parent passes, child would fail.
3. Parent fails, child passes.
4. Parent fails, child fails.

The only case where any statement can be made is case 3: "Contracts are
certainly
well-formed".
You cannot deduce the well- or ill-formedness of the contracts from any of the
other outcomes.

In fact, you have to prove that case 3 is unfulfillable to catch ill-formed
contracts.

Cheers,
-Timon
Jul 01 2011
next sibling parent reply David Nadlinger <see klickverbot.at> writes:
On 7/1/11 5:18 PM, Timon Gehr wrote:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.

 The only case where any statement can be made is case 3: "Contracts are
certainly
 well-formed".
 You cannot deduce the well- or ill-formedness of the contracts from any of the
 other outcomes.


In my opinion, one *is* able to declare the child contract invalid in 
case 2 – if the parent passes but the child fails, it certainly violates 
the »loosening« property of in contract inheritance. If you don't think 
so, could you please explain your doubts in more detail?

David
Jul 01 2011
parent Walter Bright <newshound2 digitalmars.com> writes:
On 7/1/2011 8:16 AM, David Nadlinger wrote:

 In my opinion, one *is* able to declare the child contract invalid in case 2
–
 if the parent passes but the child fails, it certainly violates the
»loosening«
 property of in contract inheritance. If you don't think so, could you please
 explain your doubts in more detail?


The rule for in contracts is:

pass = P || C;

The rule for out contracts is:

pass = P && C;
Jul 01 2011
prev sibling next sibling parent reply "Daniel Murphy" <yebblies nospamgmail.com> writes:
"Timon Gehr" <timon.gehr gmx.ch> wrote in message 
news:iukoge$u82$1 digitalmars.com...

 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.


In case 2, the contract is invalid.

In reality, the overriding graph forms a tree, and the contract is invalid 
if any precondition passes if its parent's precondition fails. (the root 
being the most derived function)

It is definately possible to implement runtime checking to enforce this.
Jul 01 2011
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Daniel Murphy wrote:

 "Timon Gehr" <timon.gehr gmx.ch> wrote in message
 news:iukoge$u82$1 digitalmars.com...

 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.


 In case 2, the contract is invalid.

 In reality, the overriding graph forms a tree, and the contract is invalid
 if any precondition passes if its parent's precondition fails. (the root
 being the most derived function)


That is case 3. And it is perfectly valid.


 It is definately possible to implement runtime checking to enforce this.


My first post on the subject features an example where case 2 can occur and be
valid. Have a look at it please.

In general:
The precondition of the parent is:

pass(in_parent)

And the precondition of the child is:

pass(in_parent) || pass(in_child)

Trivially, the precondition of the child is always fulfilled when the
precondition
of the parent is fulfilled.

What you'd want to catch is iE:

pass(in_parent) = a<=10
pass(in_child) = a<=5

Giving:
precondition of parent: a<=10
precondition of child: a<=10 || a<=5

The proposed runtime check is ineffective here, as well as completely redundant
in
the general case.

Again: in contract of child != precondition of child


Cheers,
-Timon
Jul 01 2011
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Disregard "That is case 3. And it is perfectly valid."

I had in contract and precondition mixed up there myself. sry.
Jul 01 2011
parent Timon Gehr <timon.gehr gmx.ch> writes:
Disregard
`Disregard "That is case 3. And it is perfectly valid."

I had in contract and precondition mixed up there myself. sry.`

It was actually a valid remark: It is valid for a child to loosen the
precondition.
Jul 01 2011
prev sibling parent reply "Daniel Murphy" <yebblies nospamgmail.com> writes:
"Timon Gehr" <timon.gehr gmx.ch> wrote in message 
news:iukptu$10nq$1 digitalmars.com...

 Daniel Murphy wrote:

 "Timon Gehr" <timon.gehr gmx.ch> wrote in message
 news:iukoge$u82$1 digitalmars.com...

 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.


 In case 2, the contract is invalid.

 In reality, the overriding graph forms a tree, and the contract is 
 invalid
 if any precondition passes if its parent's precondition fails. (the root
 being the most derived function)


 That is case 3. And it is perfectly valid.


Sorry for the mixin of terms, I meant parent in the tree, which is the 
opposite direction to parent in inheritance.


 It is definately possible to implement runtime checking to enforce this.


 My first post on the subject features an example where case 2 can occur 
 and be
 valid. Have a look at it please.


I disagree.  If the child's in condition requires something that the 
parent's didn't, you've just tightened the precondition.

If I understand correctly, it's equivilent to:
parent: require a is greater than 0
child: require b is greater than 0

In this case, the parent allows more values of b than the child does, so the 
precondition has been tightened.


 In general:
 The precondition of the parent is:

 pass(in_parent)

 And the precondition of the child is:

 pass(in_parent) || pass(in_child)

 Trivially, the precondition of the child is always fulfilled when the 
 precondition
 of the parent is fulfilled.

 What you'd want to catch is iE:

 pass(in_parent) = a<=10
 pass(in_child) = a<=5

 Giving:
 precondition of parent: a<=10
 precondition of child: a<=10 || a<=5

 The proposed runtime check is ineffective here, as well as completely 
 redundant in
 the general case.

 Again: in contract of child != precondition of child


Ok, I doubt I used the right terms everywhere.
Reading your other post, I'm starting to think we just have different ideas 
of how contract inheritance should work.  I _think_ mine is in line with how 
it is supposed to work in D.
If you could post some D examples that would help, doing this all in my head 
is starting to hurt.

I'm fairly confident a runtime test can catch the following case:


class A
{
    void func(int a)
    in { assert(a < 10); }
    body {}
}

class B : A
{
    void func(int a)
    in { assert(a < 5); }
    body {}
}

void main()
{
    A x = new B();

    x.func(7);
}
Jul 01 2011
next sibling parent Jesse Phillips <jessekphillips+D gmail.com> writes:
Daniel Murphy Wrote:


 I disagree.  If the child's in condition requires something that the 
 parent's didn't, you've just tightened the precondition.
 
 If I understand correctly, it's equivilent to:
 parent: require a is greater than 0
 child: require b is greater than 0
 
 In this case, the parent allows more values of b than the child does, so the 
 precondition has been tightened.


No, in this case the child has allowed more values of 'a' then the parent. If
the parent fails the child will check and say things are ok because 'b' is
greater than 0.
Jul 01 2011
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
Daniel Murphy wrote:"Timon Gehr" <timon.gehr gmx.ch> wrote in message

news:iukptu$10nq$1 digitalmars.com...

 Daniel Murphy wrote:

 "Timon Gehr" <timon.gehr gmx.ch> wrote in message
 news:iukoge$u82$1 digitalmars.com...

 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.


 In case 2, the contract is invalid.

 In reality, the overriding graph forms a tree, and the contract is
 invalid
 if any precondition passes if its parent's precondition fails. (the root
 being the most derived function)


 That is case 3. And it is perfectly valid.


 Sorry for the mixin of terms, I meant parent in the tree, which is the
 opposite direction to parent in inheritance.


 It is definately possible to implement runtime checking to enforce this.


 My first post on the subject features an example where case 2 can occur
 and be
 valid. Have a look at it please.


 I disagree.  If the child's in condition requires something that the
 parent's didn't, you've just tightened the precondition.

 If I understand correctly, it's equivilent to:
 parent: require a is greater than 0
 child: require b is greater than 0


It is equivalent to:
parent: require a is greater than 0
child: ... else require b is greater than 0



 In this case, the parent allows more values of b than the child does, so the
 precondition has been tightened.


No, the child allows arbitrary values of b if a>0, due to the short-circuiting
behavior.



[snip.]

 Again: in contract of child != precondition of child


 Ok, I doubt I used the right terms everywhere.


I didn't either :).


 Reading your other post, I'm starting to think we just have different ideas
 of how contract inheritance should work.  I _think_ mine is in line with how
 it is supposed to work in D.


I think mine is in line with how it is supposed to work, based on the following
facts:

1. It is how it currently is implemented.
2. It is how it works in Eiffel. The site on Contract Programming has a
reference
to DBC in Eiffel.
3. Yours requires that all child classes duplicate the precondition of their
parents in their in-contracts. (which will then be ensured by a runtime check.).


 If you could post some D examples that would help, doing this all in my head
 is starting to hurt.


Sure, if you remember the Foo/Qux example (Foo is parent, Qux is child, method
bar(a,b), parent requires a>0 child requires else b>0)

void main(){
  auto a=new Foo, b=new Qux;
  a.bar(1,-1);//ok
  b.bar(1,-1);//ok, child works everywhere parent works
  //a.bar(-1,1);// not ok
  //b.bar(-1,-1)// not ok
  b.bar(-1,1);//ok, child works too if b>0
}



 I'm fairly confident a runtime test can catch the following case:


Yes but that is not correct in general (unless the behavior is changed to
reflect
your ideas). The two contracts could be uncorrelated.
[snip]


Cheers,
-Timon



 Jul 01 2011



  parent reply "Daniel Murphy" <yebblies nospamgmail.com>  writes:


"Timon Gehr" <timon.gehr gmx.ch> wrote in message 
news:iukvrl$1c1c$1 digitalmars.com...

 Sure, if you remember the Foo/Qux example (Foo is parent, Qux is child, 
 method
 bar(a,b), parent requires a>0 child requires else b>0)

 void main(){
  auto a=new Foo, b=new Qux;
  a.bar(1,-1);//ok
  b.bar(1,-1);//ok, child works everywhere parent works
  //a.bar(-1,1);// not ok
  //b.bar(-1,-1)// not ok
  b.bar(-1,1);//ok, child works too if b>0
 }


And it finally clicks!  Thanks for taking the time to explain it to me.
(If only I'd got it sooner, I wouldn't have spent the last two hours 
implementing my behaviour in the compiler) 



 Jul 01 2011



  parent  Jens Mueller <jens.k.mueller gmx.de>  writes:


Daniel Murphy wrote:

 "Timon Gehr" <timon.gehr gmx.ch> wrote in message 
 news:iukvrl$1c1c$1 digitalmars.com...

 Sure, if you remember the Foo/Qux example (Foo is parent, Qux is child, 
 method
 bar(a,b), parent requires a>0 child requires else b>0)

 void main(){
  auto a=new Foo, b=new Qux;
  a.bar(1,-1);//ok
  b.bar(1,-1);//ok, child works everywhere parent works
  //a.bar(-1,1);// not ok
  //b.bar(-1,-1)// not ok
  b.bar(-1,1);//ok, child works too if b>0
 }


 
 And it finally clicks!  Thanks for taking the time to explain it to me.
 (If only I'd got it sooner, I wouldn't have spent the last two hours 
 implementing my behaviour in the compiler) 


Just found the time to go over this thread.
Thanks Daniel for asking until it was obvious for you. I now understand
it as well and I hope my initial post wasn't the cause for your
confusion. Thanks Timon for patiently answering and pushing us to
correct understanding.
The crucial thing to understand is that the in contract or precondition
is the disjunction of the super's in contract/precondition and the
statements written in "in { ... }" (note this definition is recursive).
This was pointed out several times. But I never understood why. Timon's
example makes it clear.

Jens



 Jul 05 2011



prev sibling  parent reply "Simen Kjaeraas" <simen.kjaras gmail.com>  writes:


On Fri, 01 Jul 2011 17:18:38 +0200, Timon Gehr <timon.gehr gmx.ch> wrote:


 This can be caught at runtime without a theorem prover. (And I think it
 should be)


 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.

 The only case where any statement can be made is case 3: "Contracts are  
 certainly
 well-formed".
 You cannot deduce the well- or ill-formedness of the contracts from any  
 of the
 other outcomes.

 In fact, you have to prove that case 3 is unfulfillable to catch  
 ill-formed contracts.


for a deeper hierarchy, one would simply have a bool flag - 'has a contract
passed?'. If a subsequent contract fails, the contract is in error, not the
input to the function.

Capiche?

-- 
   Simen



 Jul 01 2011



  parent reply Timon Gehr <timon.gehr gmx.ch>  writes:


Simen Kjaeraas wrote:

 On Fri, 01 Jul 2011 17:18:38 +0200, Timon Gehr <timon.gehr gmx.ch> wrote:


 This can be caught at runtime without a theorem prover. (And I think it
 should be)


 How would you catch it? I am sure it cannot be caught trivially:

 There are 4 possibilities:
 1. Both parent and child contract would pass.
 2. Parent passes, child would fail.
 3. Parent fails, child passes.
 4. Parent fails, child fails.

 The only case where any statement can be made is case 3: "Contracts are
 certainly
 well-formed".
 You cannot deduce the well- or ill-formedness of the contracts from any
 of the
 other outcomes.

 In fact, you have to prove that case 3 is unfulfillable to catch
 ill-formed contracts.


 for a deeper hierarchy, one would simply have a bool flag - 'has a contract
 passed?'. If a subsequent contract fails, the contract is in error, not the
 input to the function.

 Capiche?

 --
    Simen


All arguments given for a runtime check of this kind are the result of a
misunderstanding of contract inheritance. The 'in'-contract of an overridden
method merely extends the in-contract of the parent's method, and does not
override it. In that way, the compiler statically ensures that the precondition
of
a child cannot possibly fail if the parent's passed. Thats the sole reason for
the
short-circuiting behavior.

The child's contract says: If my parent's contract failed, I can still satisfy
the
postcondition, if this _alternative_ precondition holds. But it does not
necessarily have to pass on all input the parent passes on, because it does not
even get checked if the parent's precondition holds.

If you add such a check, the child's in-contract will have to carefully
duplicate
the parent's precondition in order not to provoke a nonsensical runtime-error.
Adding such a check would make D's contracts unusable in anything but the most
trivial cases.

(Analogously, the child's 'out'-contract does not have to re-check the parent's
postcondition.)

'Capiche?' ;)

--
   Timon



 Jul 01 2011



 next sibling parent  "Simen Kjaeraas" <simen.kjaras gmail.com>  writes:


On Fri, 01 Jul 2011 18:24:08 +0200, Timon Gehr <timon.gehr gmx.ch> wrote:


 The child's contract says: If my parent's contract failed, I can still  
 satisfy the
 postcondition, if this _alternative_ precondition holds. But it does not
 necessarily have to pass on all input the parent passes on, because it  
 does not
 even get checked if the parent's precondition holds.

 If you add such a check, the child's in-contract will have to carefully  
 duplicate
 the parent's precondition in order not to provoke a nonsensical  
 runtime-error.
 Adding such a check would make D's contracts unusable in anything but  
 the most
 trivial cases.

 (Analogously, the child's 'out'-contract does not have to re-check the  
 parent's
 postcondition.)

 'Capiche?' ;)


Absolutely. I was in the process of answering your other post where you
outlined this. Believe me, I'm on your side now. :p


-- 
   Simen



 Jul 01 2011



prev sibling next sibling parent reply "Daniel Murphy" <yebblies nospamgmail.com>  writes:


"Timon Gehr" <timon.gehr gmx.ch> wrote in message 
news:iuksb8$15l0$1 digitalmars.com...

 The child's contract says: If my parent's contract failed, I can still 
 satisfy the
 postcondition, if this _alternative_ precondition holds. But it does not
 necessarily have to pass on all input the parent passes on, because it 
 does not
 even get checked if the parent's precondition holds.


If I understand this correctly, you think the following code should be 
perfectly valid:

class A { void func(uint x) in { assert(x < 10); } body {} }
class B : A { void func(uint x) in { assert(x == 50); } body {} }

If A.func can be called with any value 0..10, why is it legal to override it 
with a function that can't accept these values?  Can you give an example 
where accepting input that is not a superset of the overriden function's 
possible input is valid? 



 Jul 01 2011



  parent  Walter Bright <newshound2 digitalmars.com>  writes:


On 7/1/2011 9:56 AM, Daniel Murphy wrote:

 If I understand this correctly, you think the following code should be
 perfectly valid:

 class A { void func(uint x) in { assert(x<  10); } body {} }
 class B : A { void func(uint x) in { assert(x == 50); } body {} }


Yes.


 If A.func can be called with any value 0..10, why is it legal to override it
 with a function that can't accept these values?


It isn't. An overriding function *must* accept all input that the overridden 
function does.

In other words, overriding functions accept a superset of the input, and
deliver 
a subset of the output.



 Can you give an example
 where accepting input that is not a superset of the overriden function's
 possible input is valid?


No.



 Jul 01 2011



prev sibling  parent  Walter Bright <newshound2 digitalmars.com>  writes:


On 7/1/2011 9:24 AM, Timon Gehr wrote:

 All arguments given for a runtime check of this kind are the result of a
 misunderstanding of contract inheritance. The 'in'-contract of an overridden
 method merely extends the in-contract of the parent's method, and does not
 override it. In that way, the compiler statically ensures that the
precondition of
 a child cannot possibly fail if the parent's passed. Thats the sole reason for
the
 short-circuiting behavior.

 The child's contract says: If my parent's contract failed, I can still satisfy
the
 postcondition, if this _alternative_ precondition holds. But it does not
 necessarily have to pass on all input the parent passes on, because it does not
 even get checked if the parent's precondition holds.

 If you add such a check, the child's in-contract will have to carefully
duplicate
 the parent's precondition in order not to provoke a nonsensical runtime-error.
 Adding such a check would make D's contracts unusable in anything but the most
 trivial cases.

 (Analogously, the child's 'out'-contract does not have to re-check the parent's
 postcondition.)



Right.



 Jul 01 2011



prev sibling  parent reply Walter Bright <newshound2 digitalmars.com>  writes:


On 7/1/2011 6:53 AM, Daniel Murphy wrote:

 To enforce this, the compiler should give an error if a base function's
 precondition passes but a derived precondition does not.


No, it should not. Only one of the contracts needs to pass.


 The requirement is not really that any 'in' contract passing is good enough,


Yes, it is.


 it's just assumed that all preconditions on inherited functions will pass if
 the base contract does.


Only one contract needs to pass.



 Jul 01 2011



  parent  "Daniel Murphy" <yebblies nospamgmail.com>  writes:


"Walter Bright" <newshound2 digitalmars.com> wrote in message 
news:iul14g$1dfs$2 digitalmars.com...

 On 7/1/2011 6:53 AM, Daniel Murphy wrote:

 To enforce this, the compiler should give an error if a base function's
 precondition passes but a derived precondition does not.


 No, it should not. Only one of the contracts needs to pass.


 The requirement is not really that any 'in' contract passing is good 
 enough,


 Yes, it is.


 it's just assumed that all preconditions on inherited functions will pass 
 if
 the base contract does.


 Only one contract needs to pass.


Yeah, I did get this eventually. 



 Jul 01 2011