From: jcm@hgc.edu (James McKim)
Subject: Re: Assertions for programming design
Organization: The Hartford Graduate Center
Date: Mon, 6 Apr 1992 13:31:48 GMT

In article <1992Apr2.214219.8863@cis.ohio-state.edu> weide@elephant.cis.ohio-state.edu (Bruce Weide) writes:
>In article <1992Mar31.125322.24280@merlin.hgc.edu> jcm@hgc.edu (James
>McKim) writes:
>>
>>Well, Richie was not referring to the STACK specification that I posted,
>>but to the following variation.
>>
>>
>>
>>class STACK[ T ]
>>
>>feature 
>>   
>>  depth : INTEGER ;
>>
>>  Create is 
>>  ensure
>>    depth = 0 ;
>>  end ; -- Create ;
>>
>>  push( x : T )  is 
>>  ensure
>>    depth = old depth + 1 ;
>>    item( depth ) = x ; 
>>  end ; -- push
>>
>>  pop is
>>  require
>>    not_empty : depth > 0 ;
>>  ensure
>>    depth = old depth - 1 ;
>>  end ; -- pop
>>
>>  item( index : INTEGER ) : T is
>>  require
>>    index_large_enough : index > 0 ;
>>    index_small_enough : index <= depth ;
>>  end ; -- item
>>
>>end ; -- STACK
>>
>> ...
>>
>>I would argue that the above specification does indeed tell what the
>>code must do but not how it must do it. The underlying data structure
>>could be an array or linked list. Most implementors would probably
>>keep track of depth "incrementally" as shown. However, there is nothing 
>>in the spec to keep you from implementing depth as a function that
>>goes out and counts the number of items in the stack each time it is
>>called.
>>
>
>Jim, I don't understand a few things about this specification.  First,

Bruce, it _does_ take some getting used to :-). The key is that, as mentioned,
in the original post, anything that is not specified as changing on a
command, does not change. Such a "no change" assumption may or may not
be automatically checkable. With this assumption, we see that push
changes depth and item(depth), but does not change item(1),..,item(depth-1).
If we imagine a bunch of pushes without intervening pops, then the first
push sets item(1), the second item(2) and so on.

 
>how do you get the top item from a stack? 

The normal "top" is item(depth). In fact, it is easy to add
"top" _without disturbing the rest of the spec_ as follows:

top : T
require depth > 0
ensure Result = item(depth)

> Second, what is the
>specification for "item"?  It requires something, but doesn't ensure
>anything.  Surely it must be specified fully in order for "push" to be
>considered specified. 

"item" is a function whose domain is changed by "push" and "pop". On
"pop" the domain shrinks, but the value of item at its remaining domain
elements does not change, hence no specification for change. On "push"
the domain expands by one integer, namely "depth". So we must specify 
item(depth). No other value of "item" has changed so again no specification
for change. I haven't been able to come up with a meaningful ensure clause
on item that doesn't give away the underlying implementation.

> Finally, is "item" something that a client of
>STACK may invoke, or is it some kind of auxiliary function that is
>just used for specification of "push"?

It's intended as part of the public interface and so is available to clients. 
Think of it as an enhanced "top". If we take as given that the public
interface of an Eiffel class is the result of applying "short" to that
class, then it is not currently possible to have item show up (outside
of a comment) in the public interface without exporting it.
>
>    -Bruce

Regards,
-- Jim
-- 

*------------------------------------------------------------------------------*
Jim McKim  (203)-548-2458     In exactly 3.2 seconds it will be a few 
Internet:  jcm@mstr.hgc.edu   minutes to 5:00.
Newsgroups: comp.lang.eiffel