Re: Eiffel and Java

[jcm@hgc.edu (James McKim)]

In article <mheaney-ya023180000111962205520001@news.ni.net> mheaney@ni.net (Matthew Heaney) writes:
>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.

Well, I've lost track of who said what. "some of" I'll buy, but I quarrel 
with either "equivalent of" (from the first line above) or "much of"
(from another poster in this thread) I quarrel with.


[... Nice example of a compass elided ...]

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

:-) FTR, Ada has some good stuff that Eiffel is currently missing, e.g.
threads.

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

Well, "just like" is too strong I think.

1) As far as I can tell the precondition is not visible to clients without
your doing yet more work.

2) The error that is raised will not be a precondition error, it'll be
a constraint error as you note. I see you can fix this with a little
more work, but that extra work is what keeps it from being "just like"
a precondition check in Eiffel.

3) The exception will be raised in the the supplier, but the onus of precondition checks is on the client and that's where the exception would be 
raised in Eiffel.

4) Perhaps most importantly, if I change the implementation of the Stack
away from an ARRAY I'd have to do yet more work to make sure that an exception
is still generated at the appropriate time and with the appropriate message.
 
>--------------------------------------------------------------------
>Matthew Heaney
>Software Development Consultant
>mheaney@ni.net
>(818) 985-1271

Hope this helps,
-- Jim


-- 

*------------------------------------------------------------------------------*
Jim McKim  (860)-548-2458     Teachers affect eternity. They can never tell 
Internet:  jcm@hgc.edu        where their influence stops.