Type Specification Examples



next up previous contents index
Next: Implementations Up: Specifications Previous: Parameterized Specifications

Type Specification Examples

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



theta-questions@lcs.mit.edu