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.7 required=5.0 tests=BAYES_00,INVALID_MSGID,
	PDS_OTHER_BAD_TLD autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,953e1a6689d791f6
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,953e1a6689d791f6
X-Google-Attributes: gid103376,public
From: mheaney@ni.net (Matthew Heaney)
Subject: Re: Eiffel and Java
Date: 1996/11/01
Message-ID: <mheaney-ya023180000111962205520001@news.ni.net>#1/1
X-Deja-AN: 193881576
references: <550sm2$sn1@buggy.news.easynet.net>
 <mheaney-ya023180002810962151220001@news.ni.net>
 <55639c$1of@buggy.news.easynet.net> <1996Oct31.201748.29073@merlin.hgc.edu>
content-type: text/plain; charset=ISO-8859-1
organization: Estormza Software
mime-version: 1.0
newsgroups: comp.lang.eiffel,comp.lang.ada
Date: 1996-11-01T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <1996Oct31.201748.29073@merlin.hgc.edu>, jcm@hgc.edu (James
McKim) wrote:

>>>Ada's type mechanism accomplishes the equivalent of pre- and
>>>post-conditions, and you don't seem to mind their inclusion in Eiffel, so
>>>that can't be it.
>>
>>Well, to some extent... I admit you can easily use pre and post conditions in 
>
>Whoa, about the simplest precondition I can think of is related to accessing
>the top of a generic stack.
>
>class STACK[G]
>...
>  top : G is
>  require
>    not_empty: depth > 0
>...
>
>How do you emulate this using types in Ada? 

Perhaps I didn't make my original point clear.  The designers of Ada 95
considered including some precondition/postcondition checking in the
language (as Eiffel does), but opted not to because Ada's rich typing
mechanisms already provide "some of" that.

For example, consider a simple abstract data type for a compass:

package Compasses is

   type Compass is limited private;

   type Heading is digits 6 range 0.0 .. 360.0;

   procedure Set_Heading (C : in out Compass; H : in Heading);
   function Get_Heading (C : Compass) return Heading;
...

The point is that it's a precondition that values for heading lie in the
range [0.0, 360.0], and Ada enforces this.  Just like a precondition it
you're setting the value, and just like a post-condition if you're getting
the value.

That subtype constraints are a form of pre- and post-condition it what I
was trying to say.  Please note that I like Eiffel and think its facilities
for checking assertions, pre-, and post-conditions are way cool and yes, I
really would like something like that in Ada.  Perhaps for the next
revision of the language.

As for how to assert precondition that a stack be non-empty, I can already
do that in Ada:

generic
   type T is private;
package Bounded_Stacks is

   type Stack (Size : Positive) is limited private;

   function Top (S : Stack) return T;

...

private

   type Item_Array is array (Positive range <>) of T;

   type Stack (Size : Positive) is
      record
         Items : Item_Array (1 .. Size);
         Top : Natural := 0;
      end record;

end;

package body Stacks is

   function Top (S : Stack) return T is
   begin
      return S.Items (S.Top);
   end;
...
end;

If the stack is empty, then S.Top = 0 and the call to function Top will
(automatically) raise Constraint_Error, because the array index constraint
was violated.

Just like a precondition.

If you don't like Constraint_Error, then put a handler for it in body of
Top and raise the exception of your choice.

--------------------------------------------------------------------
Matthew Heaney
Software Development Consultant
mheaney@ni.net
(818) 985-1271