jacob@gore.com (Jacob Gore) (10/30/90)
(If this has been discussed already, I'd appreciate a copy of the relevant articles(s).) Programming by Contract says that if C2 is a subclass of C1, then C2.r (inventing some syntax here) must be a subcontractor for C1.r (assume no renaming). This means that the precondition of C2.r must be no more restrictive than the precondition of C1.r, and the postcondition of C2.r must be no more liberal than the postcondition of C1.r . Then there's the class invariant. Class Correctness rule implies that it is both a precondition and a postcondition for every routine (except during creation). So, to keep subcontracting happy, the invariant of C2 can be neither more restrictive than that of C1 (to satisfy the subcontracting restriction on preconditions) nor more liberal (to satisfy the subcontracting restriction on postconditions). But the Parent Invariant Rule says that the invariant of C1 can be more restrictive than that of C2. Does this not conflict with subcontracting? Does this not mean that an object of class C2, when dynamically bound to a variable of type C1, may be used under conditions that violate its class's invariant? Jacob -- Jacob Gore Jacob@Gore.Com boulder!gore!jacob
bertrand@eiffel.UUCP (Bertrand Meyer) (10/31/90)
The proof rule for a routine call is roughly (see ``Introduction
to the Theory of Programming Languages'', p. 349):
{pre [argument <- i, Current <- x]} u := x.r (i) {Q [Result <- u]}
with the part relative to u removed for a procedure.
The invariant does not appear in this proof rule;
this means that only the precondition and postcondition count for the client.
The proof rule in which the invariant appears is the proof rule for
the routine body, which reads roughly
{pre & INV } do_clause {post & INV}
In less formal terms: the reason for the precondition weakening rule
is to make sure that just by doing its client's job (ensuring
the precondition) the client can obtain the contract's promises
(the postcondition) even in the presence of dynamic binding on
polymorphic entities. There should be ``no hidden clauses''.
The invariant is an internal consistency constraint on the routine;
it does not affect clients.
--
-- Bertrand Meyer
bertrand@eiffel.com