Shortcut evaluation for hierarchy of in contracts

[Timon Gehr]

Simen Kjaeraas wrote:
> 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

All arguments given for a runtime check of this kind are the result of a
misunderstanding of contract inheritance. The 'in'-contract of an overridden
method merely extends the in-contract of the parent's method, and does not
override it. In that way, the compiler statically ensures that the precondition of
a child cannot possibly fail if the parent's passed. Thats the sole reason for the
short-circuiting behavior.

The child's contract says: If my parent's contract failed, I can still satisfy the
postcondition, if this _alternative_ precondition holds. But it does not
necessarily have to pass on all input the parent passes on, because it does not
even get checked if the parent's precondition holds.

If you add such a check, the child's in-contract will have to carefully duplicate
the parent's precondition in order not to provoke a nonsensical runtime-error.
Adding such a check would make D's contracts unusable in anything but the most
trivial cases.

(Analogously, the child's 'out'-contract does not have to re-check the parent's
postcondition.)

'Capiche?' ;)

--
   Timon