Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.lang.eiffel
Subject: Re: Subcontracting vs. Parents' Invariant rule
Message-ID: <436@eiffel.UUCP>
Date: 30 Oct 90 18:30:15 GMT
References: <120020@gore.com>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 32


	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