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=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID 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: leew@micrologic.com (Lee Webber) Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/17 Message-ID: <34200ea4.13164094@wizard.pn.com>#1/1 X-Deja-AN: 273305735 References: <341eac5e.0@news.uni-ulm.de> <184347314wnr@eiffel.demon.co.uk> Organization: Pioneer Global Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-17T00:00:00+00:00 List-Id: On Tue, 16 Sep 1997 21:25:35 GMT, bobduff@world.std.com (Robert A Duff) wrote: >In article <184347314wnr@eiffel.demon.co.uk>, >Roger Browne wrote: >>The client doesn't need to examine the invariant directly, because the >>invariant must be satisfied any time the object is accessible to the client. > >My understanding is that the compiler generates run-time checks for >invariants at both entry to and exit from each feature. Is that >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? What you say is true, I believe, if the object possesses what Bertrand Meyer calls "referential integrity", which among other things means that its state only changes as a result of the application of one of its features. (I am not famiiliar with this term in its mathematical context, so I am treating it as if it were a newly defined concept.) While this is so highly desirable a property of an object that some (including Meyer) would like to enforce it if they could, there are circumstances in which it is inappropriate if not impossible. The standard case is that of an object encapsulating an external entity (e.g., a communications port) which itself changes state arbitrarily. In this case, you often can only maintain referential integrity by discarding important state information (which, sadly, many communications drivers do), or by declaring that the unanticipated state change is nonetheless unexceptional. Be that as it may, Eiffel doesn't enforce r.i. and therefore must check the invariant on feature entry as well as exit.