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

5.1. Pre & Post Conditions

Preconditions:
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.

Postconditions:
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.
Note: 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.

5.2. Operations

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 implementation details.

It is useful to divide operations into four kinds of functions:

  1. Those that create stacks out of non-stacks, e.g. CREATE_STACK, READ_STACK, CONVERT_ARRAY_TO_STACK

  2. Those that `destroy' stacks (opposite of create) e.g. DESTROY_STACK

  3. Those that `inspect' or `observe' a stack, e.g. TOP, IS_EMPTY, WRITE_STACK

  4. Those that takes stacks (and possibly other things) as input and produce other stacks as output, e.g. PUSH, POP
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.
At this point, go through the Stack Specification line by line.

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 that implements POP?

Either way is possible. Here are the pros and cons of the 2 possibilities:

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 following: 
        PUSH(S,1);
        POP(S);
It is obvious that there is no need to check if S is empty - this precondition of POP is guaranteed to be satisfied because it is a postcondition of PUSH.

Implementation Checks Preconditions

There are several advantages to having the implementation check its own preconditions:
  1. 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.

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

  3. 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 our program.
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 and robustness.

An additional possibility is to selectively include or exclude the implementation's condition checking code, e.g. using #ifdef: 

#ifdef SAFE
    if (! condition) error("condition not satisfied");
#endif
This code will get included only if we supply the -DSAFE argument to the compiler (or otherwise define SAFE). Thus, in an application where the user checks carefully for all preconditions, we have the option of omitting all checks by the implementation.

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:
Formality
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 data structures.