Stack Specification
A stack is either empty or it
consists of two parts:
- a top element
- a stack (the remaining elements).
The elements in a stack may be of any type, but all the elements in a
given stack must be the same type.
The operations on stacks are:
create_stack
-
- Inputs: none
- Outputs: S (a stack)
- Preconditions: none
- Postconditions: S is defined and empty
destroy_stack
-
- Inputs: S (a stack)
- Outputs: S' (i.e. S changed)
- Preconditions: none
- Postconditions: S' is undefined. All resources (e.g.
memory) allocated to S have been released. No stack
operation can be performed on S'.
is_empty
-
- Inputs: S (a stack)
- Outputs:
is_empty (boolean)
- Preconditions: none
- Postconditions:
is_empty is true iff S is
empty.
top
-
- Inputs: S (a stack)
- Outputs: E (a stack element)
- Preconditions: S is not empty
- Postconditions: E is the top element on S (S is unchanged)
pop
-
- Inputs: S (a stack)
- Outputs: S' (i.e. S is changed)
- Preconditions: S is not empty
- Postconditions: Because S is not empty, it consist of two
parts: a top element T and a stack R of remaining
elements. S'=R.
push
-
- Inputs: S (a stack) and V (a value)
- Outputs: S' (i.e. S changed)
- Preconditions: V is of appropriate type for an element of
S
- Postconditions: S' has V as its top element and S as its
remaining elements.