Shortcut evaluation for hierarchy of in contracts

[Timon Gehr]

Daniel Murphy wrote:"Timon Gehr" <timon.gehr at gmx.ch> wrote in message
>news:iukptu$10nq$1 at digitalmars.com...
>> Daniel Murphy wrote:
>>> "Timon Gehr" <timon.gehr at gmx.ch> wrote in message
>>> news:iukoge$u82$1 at 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