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: Joachim Durchholz Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/20 Message-ID: <3423CD89.F0B7B91E@munich.netsurf.de>#1/1 X-Deja-AN: 274576373 References: <341FB47D.1B81@stratus.com> X-Priority: 3 (Normal) Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-20T00:00:00+00:00 List-Id: Robert A Duff wrote: > 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"). Well, you can also count on a postcondition always to be fulfilled at end-of-routine, still they may not and raise an exception. The point is that you can count on Eiffel assertions to be valid whenever they are relevant. An invariant is relevant as soon as a routine accesses the object, not earlier. > 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! Such invariant violations are programming errors. The error is at the point that changes the object; for efficiency reasons, the detection of this error is postponed until the object is actually used again. It would be no big deal to allow for invariant checking whenever appropriate. The run-time system would have to keep a record on which object depends on which other objects for its invariant; whenever an object changes, the appropriate invariants would be rechecked. (I'd really like to see an Eiffel system that does this!) If an invariant references an externally accessible object you better make sure that these aliasing access paths aren't abused! You can control this via two strategies: 1) Don't give away references to your private, invariant-relevant objects. 2) If you can't stick to (1), give the references only to your friends (i.e. classes that you write yourself, via selective export). 3) If you can't stick to (2), create a wrapper class around the reference that you're giving away and check the routines in that wrapper class so that they cannot violate the invariant. So while the language doesn't prevent you from violating invariants, you can keep the problem under control. Regards, Joachim -- Please don't send unsolicited ads.