Specification
Example:
specification of stacks
- Preconditions:
- properties of the inputs assumed by an operation.
- Postconditions:
- the effects of a operation.
Operations:
it is useful to distinguish between operations that...
- create stacks:
create_stack
- destroy stacks:
destroy_stack
- inspect stacks:
top, is_empty
- modify stacks, or take stacks and produce new ones:
push, pop