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: rodemann@mathematik.uni-ulm.de (Joerg Rodemann) Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/16 Message-ID: <341eac5e.0@news.uni-ulm.de>#1/1 X-Deja-AN: 272980409 References: Followup-To: comp.lang.ada,comp.lang.eiffel Organization: University of Ulm, SAI, Germany Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-16T00:00:00+00:00 List-Id: Don Harrison (nospam@thanks.com.au) wrote: > private > type Root_Stack is abstract tagged record > ... > invariant > Full (Current) implies not Empty (Current); > Empty (Current) implies not Full (Current); > end record; > end Pkg; Well, this is a solution that seems possible to me. Of course anything the invariant depends on has to be declared within the the spec although this might be in the private part. This should not be a problem since it seems quite convenient among Ada programmers to declare everything before use. Thus invariants should be preceded by the declaration of any variable or method used for its definition. A short question on the side to our Eiffel friends: are the Eiffel invariants visible to the client or are the just there to ensure object state consistency so that it is able to recognize an error condition? I. e. I assume they may rely on private member variables, don't they? > :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 agree that the concept to be most difficult to be introduced into Ada are the postconditions due to the problem of value changes during execution of a method. This example made it quite obvious to me although I mentioned this problem already within another post earlier. Regards Joerg -- rodemann@mathematik.uni-ulm.de | Dipl.-Phys. Joerg S. Rodemann Phone: ++49-(0)711-5090670 | Flurstrasse 21, D-70372 Stuttgart, Germany -------------------------------+--------------------------------------------- rodemann@rus.uni-stuttgart.de | University of Stuttgart, Computing Center Phone: ++49-(0)711-685-5815 | Visualization Department, Office: 0.304 Fax: ++49-(0)711-678-7626 | Allmandring 30a, D-70550 Stuttgart, Germany