From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: nospam@thanks.com.au (Don Harrison)
Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp:
 process issue?)
Date: 1997/09/18
Message-ID: <EGot0J.3y0@syd.csa.com.au>#1/1
X-Deja-AN: 273468390
Sender: news@syd.csa.com.au
References: <341FB47D.1B81@stratus.com>
Reply-To: nospam@thanks.com.au
X-Nntp-Posting-Host: dev50
Organization: CSC Australia, Sydney
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-09-18T00:00:00+00:00
List-Id: <comp.lang.ada>


Franck Arnaud wrote:

:Robert A Duff:
:
:> My understanding is that the compiler generates run-time checks for
:> invariants at both entry to and exit from each feature.
:
:Correct.
:
:>  If so, why?  How can the check-upon-entry ever fail, since the
:> invariant must be true initially, and must be true after every exit?
:
:If the invariant is other.some_condition, other's state may have changed
:since last time.

If I understand you correctly, you're saying that if our class has an 
invariant containing a condition "other.some_condition" where "other" is 
an attribute common to our class and another class, then updating the common 
object via the other class won't check the invariant in our class. Correct?

Hence, it must be re-checked before executing any operation.


Don.                     (Reverse to reply)
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             au.com.csa.syd@donh