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/26 Message-ID: #1/1 X-Deja-AN: 275677349 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: Organization: CSC Australia, Sydney Reply-To: nospam@thanks.com.au Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-26T00:00:00+00:00 List-Id: Matt Heaney wrote: :In article , Don Harrison wrote: : :> type Unbounded_Queue is :> tagged record :> ... :> invariant :> Internally_Consistent (Current); :> end record; :> :>Somewhere: :> :> if Internally_Consistent (Q) then .. : :You could run with this idea and use something similar to controlled types, :or you could use an attribute idea. Every type could be born with an :invariant function that is called just before executing the body of an :operation, and called just after executing the body. Interesting ideas. I'll need to remind myself of what controlled types are to fully appreciate the possibilities. :private : :function Internally_Consistent (Q : Unbounded_Queue) return Boolean; : -- this would be analogous to overriding Initialize for a Controlled type Perhaps, you would want to explicitly associate this with Initialise. :type Unbounded_Queue is new Root_Queue with : record : ... : end record; : :for Unbounded_Queue'Invariant use Internally_Consistent; : -- an alternate technique that uses an attribute, not unlike stream I/O :subprograms : :end; : :Though I haven't quite figured out what happens when you derive from :Unbounded_Queue. I agree, that's an issue. :Can you override your parent's invariant? In Eiffel, you can by encapsulating it in a function, and, in the descendant, overriding the function and omitting the invariant declaration. In the parent: some_boolean_function: BOOLEAN is .. ... invariant some_boolean_function end In the descendant: redefine some_boolean_function ... some_boolean_function: BOOLEAN is .. -- overridden ... end The overriding should always *strengthen* the condition. It is naughty to weaken it. In the case of a descendant that *does* contain an invariant, the condition is and-ed with the parent's. :Under what circumstances would that make sense? When the descendant is a more restrictive variant of the parent. P.S. I'm on leave for two weeks, so won't be able to respond till then. Don. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Don Harrison donh at syd.csa.com.au