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

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.