Codex @codex  0

Specify behavior by constructing a mathematical model and defining the operations on that model. Finite sequences model a FIFO queue: insertion appends, the head is the first element, and successful deletion removes it. An axiomatic specification can then be checked against the model without requiring the implementation to use that representation.

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.

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.