Lecture 1 - Specification
5. Specification (Sections 3.3 & 3.5)
- Handout Stack Specification.
Handout: Stack Specification
Let us now look in detail at how we specify an abstract
datatype. We will use `stack' as an example.
The data structure stack is based on the everyday notion of a
stack, such as a stack of books, or a stack of plates. The defining
property of a stack is that you can only access the top
element of the stack, all the other elements are underneath the top
one and can't be accessed except by removing all the elements above
them one at a time.
The notion of a stack is extremely useful in computer science, it
has many applications, and is so widely used that microprocessors
often are stack-based or at least provide hardware implementations of
the basic stack operations.
We will briefly consider some of the applications later. First, let
us see how we can define, or specify, the abstract concept of a stack.
The main thing to notice here is how we specify everything needed in
order to use stacks without any mention of how stacks will be
5.1. Pre & Post Conditions
- These are properties about the inputs that are assumed by an
operation. If they are satisfied by the inputs, the operation is
guaranteed to work properly. If the preconditions are not
satisfied, the operation's behaviour is unspecified: it might
work properly (by chance), it might return an incorrect answer,
it might crash.
- Specify the effects of an operation. These are the only
things you may assume have been done by the operation. They are
only guaranteed to hold if the preconditions are satisfied.
The definition of the values of type `stack' make no mention of an
upper bound on the size of a stack. Therefore, the implementation
must support stacks of any size. In practice, there is
always an upper bound - the amount of computer storage available.
This limit is not explicitly mentioned, but is understood - it is an
implicit precondition on all operations that there is storage
available, as needed. Sometimes this is made explicit, in which case
it is advisable to add an operation that tests if there is
sufficient storage available for a given operation.
The operations specified on the handout are core operations -
any other operation on stacks can be defined in terms of these ones.
These are the operations that we must implement in order to implement
`stacks', everything else in our program can be independent of the
It is useful to divide operations into four kinds of functions:
A specification must say what an operation's input and outputs are,
and definitely must mention when an input is changed. This
falls short of completely committing the implementation to procedures
or functions (or whatever other means of creating `blocks' of code
might be available in the programming language). Of course, these
details eventually need to be decided in order for code to actually be
written. But these details do not need to be decided until
code-generation time; throughout the earlier stages of program design,
the exact interface (at the code level) can be left unspecified.
- Those that create stacks out of non-stacks, e.g.
- Those that `destroy' stacks (opposite of create) e.g.
- Those that `inspect' or `observe' a stack, e.g.
- Those that takes stacks (and possibly other things) as input and
produce other stacks as output, e.g.
- At this point, go through the Stack Specification line by
5.3. Checking Pre & Post Conditions
It is very important to state in the specification whether each
precondition will be checked by the user or by the implementer. For
example, the precondition for
POP may be checked either
by the procedure(s) that call
POP or within the procedure
Either way is possible. Here are the pros and cons of the 2
User Guarantees Preconditions
The main advantage, if the user checks preconditions - and
therefore guarantees that they will be satisfied when the core
operations are invoked - is efficiency. For example, consider the
It is obvious that there is no need to check if
empty - this precondition of
POP is guaranteed to be
satisfied because it is a postcondition of
Implementation Checks Preconditions
There are several advantages to having the implementation
check its own preconditions:
There are arguments on both sides. The textbook specifies that
procedures should signal an error if their preconditions are not
satisfied. This means that these procedures must check their own
preconditions. That's what our model solutions will do too. We will
thereby sacrifice some efficiency for a high degree of maintainability
- It sometimes has access to information not available to the user
(e.g. implementation details about space requirements), although
this is often a sign of a poorly constructed specification.
- Programs won't bomb mysteriously - errors will be detected (and
reported?) at the earliest possible moment. This is not true
when the user checks preconditions, because the user is human
and occasionally might forget to check, or might think that
checking was unnecessary when in fact it was needed.
- Most important of all, if we ever change the specification, and
wish to add, delete, or modify preconditions, we can do this
easily, because the precondition occurs in exactly one place in
An additional possibility is to selectively include or exclude the
implementation's condition checking code, e.g. using
if (! condition) error("condition not satisfied");
This code will get included only if we supply the
argument to the compiler (or otherwise define
Thus, in an application where the user checks carefully for all
preconditions, we have the option of omitting all checks by the
5.4. Difference Between Textbook & Class
The specifications I will give you differ slightly from those you will
see in the textbook. The differences are:
- Pre- and postconditions must be precisely stated, they
are of no use if they are ambiguous. I have used English
whenever it is precise, whereas the textbook is inclined to
state these conditions with mathematical formulae. It is also
more thorough than I am: it attempts to give the full `Axiomatic
Semantics' of the operations. This involves stating properties
that I leave implicit. For example, it explicitly specifies that
IS_EMPTY( CREATE_STACK () )
should always be true. Ideally, these axioms fully define all
aspects of the behaviour of the operations. They are very
useful, I encourage you to study the textbook's specifications
for the data structures we investigate.
- Memory management
- My specifications include a statement about the effect of an
operation on the memory used to store a data structure (e.g. see
DESTROY_STACK). This will be a particularly
important part of the specification in a few weeks, when we
start using pointers and dynamically-allocated memory for our