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 element
Note 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 stack
The 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".