Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ncar!boulder!gore!jacob
From: jacob@gore.com (Jacob Gore)
Newsgroups: comp.lang.eiffel
Subject: Re: Invariant rule
Message-ID: <120013@gore.com>
Date: 10 Feb 90 04:54:00 GMT
References: <240@eiffel.UUCP>
Reply-To: jacob@gore.com (Jacob Gore)
Organization: Gore Enterprises
Lines: 19

/ comp.lang.eiffel / bertrand@eiffel.UUCP (Bertrand Meyer) / Feb  8, 1990 /
> > 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}

Yes, but if I understand the change correctly, a creation routine may be
exported, in which case it also falls under the rule for exported routines:

	{INV and pre_c} c {INV and post_c}

So, should there be a distinction between a creation routine being invoked
during creation vs. it being invoked with a call?

Jacob
--
Jacob Gore		Jacob@Gore.Com			boulder!gore!jacob