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: schlegel@Informatik.Uni-Rostock.de (Juergen Schlegelmilch) 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: 273530821 References: <341FB47D.1B81@stratus.com> Organization: University of Rostock, Germany Reply-To: schlegel@Informatik.Uni-Rostock.de Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-18T00:00:00+00:00 List-Id: On Thu, 18 Sep 1997 12:48:25 GMT, Robert A Duff wrote: >Franck Arnaud wrote: >: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. If 'other' is not exported to any other class, and if there is no method that allows clients to obtain a reference to (the object bound to) 'other', and if 'other' is always bound to an object created locally (i.e. not to an object that came into scope as a routine argument, directly or via some intermediate object), then the only access path to that object is through the current object and the invariant is valid. There are quite a lot 'if' statements above. Other languages have a special type called 'unique ref' that guaranties that there is always only one object referencing the target. However, since all the 'if's are in the hands of the programmer implementing the class with the invariant in question, I think we don't need language support for this design pattern. So let them reference other objects in invariants; and if it breaks, its their own fault for not obeying proper design rules :-) Just my $0.02. Juergen -- +-----------------------------------------------------------------------------+ Dipl.-Inf. Juergen Schlegelmilch University of Rostock email: schlegel@Informatik.Uni-Rostock.de Computer Science Department http://www.informatik.uni-rostock.de/~schlegel Database Research Group Tel: ++49 381 498 3402 18051 Rostock Fax: ++49 381 498 3426 Germany +-----------------------------------------------------------------------------+