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: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
From: Owen Fellows <ofellows@calfp.co.uk>
Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp:
 process issue?)
Date: 1997/09/16
Message-ID: <341EB601.711526FF@calfp.co.uk>#1/1
X-Deja-AN: 273004916
References: <mheaney-ya023680001009971956580001@news.ni.net>
 <EGLBMK.A5I@syd.csa.com.au> <341eac5e.0@news.uni-ulm.de>
X-NNTP-Posting-Host: calfp.demon.co.uk [158.152.70.168]
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-09-16T00:00:00+00:00
List-Id: <comp.lang.ada>


Joerg Rodemann wrote:
> 
> 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?

They may, but I don't think they should. In the same way with pre and
post conditions
you don't want to have implementation details exposed.

So for a stack 

   extend (item: T) is  
      require
         not empty
   ....


is better than
  
   extend (item: T) is  
      require
         array.count < array.capacity
   ....

If you find yourself exposing implementation in the way you mention, it
is
very likely you have missed a useful feature, in the above example,
empty: BOOLEAN


> > :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.
>