Shortcut evaluation for hierarchy of in contracts

[Simen Kjaeraas]

On Fri, 01 Jul 2011 17:18:38 +0200, Timon Gehr <timon.gehr at 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