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: bobduff@world.std.com (Robert A Duff) Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/18 Message-ID: #1/1 X-Deja-AN: 273521119 References: <341FB47D.1B81@stratus.com> Organization: The World Public Access UNIX, Brookline, MA Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-18T00:00:00+00:00 List-Id: 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. It seems to me that such an invariant is not invariant. I thought the whole point of invariants was that you can count on the invariant "always" being true (where "always" really means "always, except while the object is in the process of being updated"). But if invariants are allowed to referent other.some_condition, and "other" can be modified willy-nilly by who-knows-what software, then such an invariant is not invariant at all! Note the conceptual difference between preconditions and invariants -- it's the responsibility of the client to make sure a precondition is true before calling something, but it's *supposedly* the responsibility of the class itself to maintain its own invariants. - Bob