First we specify a simple "bag" abstraction and two creation routines for "bag"s:

bag = type [T] put (x: T) % effects adds x to the bag get ( ) returns (T) signals (empty) % effects removes and returns an arbitrary element of the bag % signals empty if bag is empty size ( ) returns (int) % effects returns the number of elements in the bag copy ( ) returns (bag[T]) where T has copy( ) returns (T) % effects returns a new bag containing copies of the elements of self end bag create_bag [T] ( ) returns (bag[T]) % effects returns a new, empty bag singleton_bag [T] (x: T) returns (bag[T]) % effects returns a new bag containing x as its only elementNote in the specification of "copy" the use of self to refer to the method's object. Note also that the "copy" method imposes a constraint on "T" whereas the "bag" type has no constraint on "T"; "copy" is an optional method (3.2.2).

Next we specify type "stack", a subtype of "bag":

stack = type [T] < bag[T] {push for put, pop for get} push (x: T) % effects adds x to the top of the stack pop ( ) returns (T) signals (empty) % effects removes and returns the top element of the stack % signals empty if stack is empty top ( ) returns (T) signals (empty) % effects returns top element of the stack % signals empty if stack is empty copy ( ) returns (stack[T]) where T has copy ( ) returns (T) % effects returns a new stack containing copies of the elements of self % in the same order as in self. end stack create_stack [T] ( ) returns (stack[T]) % effects returns a new, empty stackThe specification of "stack" introduces a new method, "top". It contains specifications for "push" and "pop", since they constrain the behavior of the corresponding "bag" methods, and for "copy", since it has a different signature and specification than its counterpart, but it omits the specification of "size", since it would be identical to its counterpart. Note that there are two creation routines for "bag" but only one for "stack".

theta-questions@lcs.mit.edu