Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming (resit) / 7

An abstract data type specifies a collection of values and permitted operations through their observable behavior, independently of how those values are represented. A FIFO queue can therefore have linked-list or array implementations while satisfying the same abstract contract.

An axiomatic specification describes operations by laws and relationships among their results, without choosing a representation. A constructive specification gives a mathematical model and defines the operations on it: for example, represent queues by finite sequences, append at the end, and remove the first element. A constructive specification need not expose a machine-level implementation.

Use tagged disjoint unions for results that can contain either a value or an error message. This avoids ambiguity even if the item set itself contains the string Empty queue. The operation signatures areHere $1$ is a singleton, expressing that create takes no meaningful argument. Write successful results as ${\mathrm{ok}}_I(i)$ and ${\mathrm{ok}}_Q(q)$, and errors as ${\mathrm{err}}_I(e)$ and ${\mathrm{err}}_Q(e)$ for $e=\text{Empty queue}$. Returning an error is not returning a queue, so its result must not be silently passed to another queue operation.

Write $q_0=\mathrm{create}()$ and $e=\text{Empty queue}$. The axiomatic specification starts withFor insertion at the tail, the head laws areThe deletion laws areRequire that queues are generated from create by finitely many add operations, with the usual equality of indistinguishable queue values. Induction on that construction ensures that the nonempty deletion case supplies a successful queue result, so the last law is well-typed and covers all nonempty queues.

These equations express the behavior of a FIFO queue: adding to a nonempty queue changes neither its existing head nor the order of its remaining items. As a consistency model, interpret $Q$ as finite sequences, create as the empty sequence, add as append, and successful head/delete as first-element/tail operations. This model satisfies every displayed law and distinguishes error messages from ordinary items.