Re: Eiffel and Java

[jsa@alexandria (Jon S Anthony)]

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

> In article <55639c$1of@buggy.news.easynet.net> Sacha@easynet.fr (Vincent WEBER) writes:
> >In article <mheaney-ya023180002810962151220001@news.ni.net>, mheaney@ni.net 
> >says...
...
> >>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? 

This is not a particularly good example of not having full assertions in 
standard Ada as it is rather easy to "emulate":

    type Stack is private;
...
    type Depth_Range is new Natural;

    type Stack is record
        Depth : Depth_Range := Depth_Range'First;
        ...
    end record;
...
    function Top (S : Stack) return ...
        Not_Empty : Positive := S.Depth; -- Requires Depth > 0 or CE is raised
...


> Just askin'
> -- Jim

Just answerin'

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
Belmont, MA 02178
617.484.3383
jsa@organon.com