Shortcut evaluation for hierarchy of in contracts

[Daniel Murphy]

"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

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);
}