Re: Eiffel and Java

[mheaney@ni.net (Matthew Heaney)]

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