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: mheaney@ni.net (Matthew Heaney) Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/25 Message-ID: #1/1 X-Deja-AN: 275476547 References: Organization: Estormza Software Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-25T00:00:00+00:00 List-Id: In article , Don Harrison wrote: >:So I'm not clear that operations are even needed to implement an invariant, >:if one accepts the model that invariants are simply boolean expressions >:comprising only record components. > >Yes, it's true they aren't necessary, though they are *helpful*. For example, >if the condition defined by your invariant was useful elsewhere, you could >encapsulate it in a function and reuse it: > > function Internally_Consistent (Queue: Unbounded_Queue) return Boolean is > begin > ... -- return a boolean reflecting Matt's invariant > end; Once again, you're one step ahead of me. I had exactly this idea after I had made my post. > 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. private function Internally_Consistent (Q : Unbounded_Queue) return Boolean; -- this would be analogous to overriding Initialize for a Controlled type 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. Can you override your parent's invariant? Under what circumstances would that make sense? -------------------------------------------------------------------- Matthew Heaney Software Development Consultant (818) 985-1271