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/20 Message-ID: #1/1 X-Deja-AN: 274200575 References: Organization: Estormza Software Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-20T00:00:00+00:00 List-Id: In article , nospam@thanks.com.au wrote: >One issue to consider is whether to include preconditions and postconditions >in separate operation declarations - doing so would only worsen the >redundancy problem but not doing so creates an inconsistency similar to Pascal >"forward" declarations. :( > Yes, I would include preconditions and postconditions in separate operation declarations. But I'm not sure what you mean by a "redundancy problem." o If you mean the overloaded subprograms each have to list potentially identical pre and post-conditions, then I don't have any problem with that. o If you mean list pre and postconditions again in the package body, I would say you don't need to bother (but there may be issues about that that I haven't considered). >:I still have to think about how to state a representation invariant. Its >:specification would somehow have to be attached to the full view of the >:type, and would be evaluated at exit from a subprogram. > >What is meant by "the full view of the type"? Do you mean including the >operations in the package body? - this would be close to the Eiffel concept. The full view of a type is the type declaration that appears after the word "private" in the spec, ie: generic type Stack_Item; Max_Depth : Positive; package Stacks_G is -- This is the "partial" view: type Bounded_Stack is tagged private; ... private type Stack_Item_Array is array (Positive range 1 .. Max_Depth) of Stack_Item; -- This is the "full" view: type Bounded_Stack is tagged record Items : Stack_Item_Array; Depth : Natural := 0; end record; end; >Unless I'm mistaken, you're faced with a dilemma in trying to implement >invariants: > >1) On the one hand, you want to allow invariants to include all of the > type's operations declared in a package - exported and hidden, primitive > and class-wide - it implies declaring them in the package body somehow. > While such invariants could use the "full" view of the type, they > wouldn't be visible to public child packages. This would make it > impossible to extend an invariant in a descendant type in a public child. Actually, I hadn't considered using operations in the invariant. What I had in mind is a relationship among the variables that are the representation of an object. As these variables are part of the implementation, my thinking was that no public operations would apply. For example, I have a queue implemented as a linked list, with a pointer to the front of the list, and a pointer to the back. I would like to state as a representation invariant that the previous pointer of the front node is null, and the next pointer of the back node is also null: generic type Queue_Item is private; package Queues_G is type Unbounded_Queue is tagged private; ... private package Queue_Item_Lists is new Lists_G (Queue_Item); use Queue_Item_Lists; type Unbounded_Queue is tagged record Front, Back : Unbounded_List; Length : Natural := 0; invariant Front_OK : Length /= 0 implies Front.Previous = null; Back_OK : Length /= 0 implies Back.Next = null; Length = 0 implies Front = null and Back = null; Length = 1 implies Front = Back; Length > 1 implies Front /= Back; end record; 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. >:I also haven't thought of a convenient way to state a postcondition in >:terms of a change in a value (ie the length before the call versus the >:length after the call). > >Do you mean like the following?.. > >procedure Remove_Item > (Sequence : in out Root_Sequence; > Index : in Positive) >precondition > Is_Present: Index <= Length (Sequence); >postcondition > Shorter: Length (Sequence) < Length (Sequence'Old) >end; I like this idea. >Don. (Reverse to reply) >=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- >Don Harrison au.com.csa.syd@donh Can you fix this so I don't have to do some much damn editing reply to you? How about donh*syd.csa.com.au syd.csa.com.au@donh Thank you! -------------------------------------------------------------------- Matthew Heaney Software Development Consultant (818) 985-1271