Shortcut evaluation for hierarchy of in contracts

[Timon Gehr]

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 at gmx.ch> wrote in message
> news:iuklvm$pks$1 at 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