Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!mcgill-vision!bloom-beacon!bu.edu!bu-cs!snorkelwacker!usc!ucsd!hub!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.lang.eiffel
Subject: Invariant rule
Message-ID: <240@eiffel.UUCP>
Date: 9 Feb 90 01:10:43 GMT
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 20

In message <226@eiffel.UUCP>, jacob@gore.com (Jacob Gore) asks
with respect to the new form of creation operations (see
``Eiffel cleanup #1: The creation mechanis,'', <226@eiffel.UUCP>):

> How exactly will the Invariant Rule read after this change?  (It now
> specifies a special case for the Create procedure.)

Clearly, every creation procedure c must satisfy

    {defaults and pre_c} c {INV and post_c}

where pre_c is the precondition of c, post_c is its postcondition,
defaults is an assertion characterizing the
object state resulting from default initializations,
and INV is the class invariant. 


-- 
-- Bertrand Meyer
bertrand@eiffel.com