Re: Invariant rule

Article View: comp.lang.eiffel

Article #1553

#1553

From: Jacob Gore
Date: Sat, 10 Feb 1990 04:54

19 lines
1043 bytes

/ 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

Technical Details

Message-ID: <120013@gore.com>

Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ncar!boulder!gore!jacob

References: <240@eiffel.UUCP>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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

Reply to Parent Message