Specification

A specification is a precise statement of what a program or algorithm must do. It lists the legal inputs with a precondition and it states the right outputs for each of them with a postcondition. A program is correct when it meets its specification.

Definition

Let $X$ be a set of inputs and $Y$ a set of outputs. A specification is a pair $(P, Q)$ where $P \subseteq X$ is a precondition and $Q \subseteq X \times Y$ is a postcondition. Write $P(x)$ for $x \in P$ and $Q(x, y)$ for $(x, y) \in Q$. A program $A$ meets $(P, Q)$ when

This is total correctness. The program is partially correct for $(P, Q)$ when $\forall x \in X : \big( P(x) \wedge A \text{ stops on } x \big) \Rightarrow Q(x, A(x))$. The stop is a hypothesis here and not a goal. See partial correctness. Total correctness is partial correctness plus termination on each $x$ with $P(x)$. A specification says what the program computes and does not say how. Many programs can meet the same specification.

The relation $Q$ may allow several outputs for one input. Then the specification is non-deterministic, and a program may return any of them. If for each $x$ with $P(x)$ there is exactly one $y$ with $Q(x, y)$, then $Q$ defines a function on $P$. The opposite case is a pitfall. If some $x$ with $P(x)$ has no $y$ with $Q(x, y)$, then no program meets $(P, Q)$. A good specification is satisfiable: $\forall x \,(P(x) \Rightarrow \exists y \, Q(x, y))$.

Examples and non-examples

• Integer square root. $X = Y = \mathbb{Z}$. $P(n)$ is $n \ge 0$. $Q(n, r)$ is $r^2 \le n < (r+1)^2$. For each $n \ge 0$ there is exactly one such $r$. Proof. Each solution is non-negative: from $r^2 \le n < (r+1)^2$ we get $r^2 < (r+1)^2$, so $2r + 1 > 0$ and $r \ge 0$. Existence: the set of $r \ge 0$ with $r^2 \le n$ holds $0$, and each element is at most $\max(n, 1)$ because $r \le r^2$ for an integer $r \ge 1$, so the set has a largest element $r$. Then $r + 1$ is not in the set, so $(r+1)^2 > n$. Uniqueness: if $0 \le r_1 < r_2$ both satisfied $Q$ for $n$, then $r_1 + 1 \le r_2$ and $(r_1+1)^2 \le r_2^2 \le n < (r_1+1)^2$, a contradiction. The program ISQRT of the page on correctness meets it.
• Sorting. $X = Y$ is the set of finite arrays of numbers. $P$ is true. $Q(A, B)$ says that $B$ is a permutation of $A$ and $B[0] \le B[1] \le \cdots$. See the sorting problem.
• Search in a sorted array (non-deterministic). $P(A, key)$: $A$ is non-decreasing. $Q(A, key, i)$: either $0 \le i < m$ and $A[i] = key$ (with $m$ the length of $A$), or $i = -1$ and $key$ does not occur in $A$. When $key$ occurs twice, two outputs are right. The binary search returns one of them.
• Non-example: too weak. $Q(n, r)$ is $r^2 \le n$. The constant program $r = 0$ meets it for each $n \ge 0$. The pair $(P, Q)$ is a specification in the sense above, but it does not describe integer square root. Compare $n = 10$: both $r = 0$ and $r = 3$ meet it, and only $r = 3$ meets the exact one.
• Non-example: not satisfiable. Take $P$ = true for integer square root, with the same $Q$. For $n = -1$ no $r$ has $r^2 \le -1$, so no program meets this pair. The precondition $n \ge 0$ removes the problem.
• Non-example: not precise. "Return a number close to $\sqrt n$" is not a specification. No test or proof can decide whether $r = 2$ is close enough for $n = 10$.
• Non-example: a method. "Search for $r$ by halving an interval" describes an algorithm. It does not say what the result must satisfy.

Related definitions

• Precondition: the first half of a specification, the assumption on the input.
• Postcondition: the second half, the guarantee on the output.
• Hoare triple: a specification written as $\{P\}\ S\ \{Q\}$ for a program text $S$.
• Partial correctness and total correctness: the two ways in which a program can meet a specification.
• Design by contract: a method where the specification of each routine is part of its code.
• Weakest precondition: the largest precondition under which a program meets a given postcondition.

References

1. Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, fourth edition, Section 1.1
2. C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM 12(10) (1969), pp. 576 to 580