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