Shortcut evaluation for hierarchy of in contracts

[Timon Gehr]

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.

>
> 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