Algorithm correctness

An algorithm is correct with respect to a specification when, for every input that the specification allows, it stops and gives an output that the specification accepts. Correctness is a claim about all legal inputs. There are usually infinitely many of them, or too many to try, so a finite set of tests cannot prove it. A proof can. It has two parts: partial correctness (the output is right if the algorithm stops) and termination (the algorithm does stop). Together they give total correctness.

In plain words

You cannot call an algorithm correct until you say what it must do. The statement of that task is the specification. It says which inputs are legal and which outputs are right for each of them.

An algorithm is then correct when two things hold for every legal input. It stops, and its output is right. A test runs the algorithm on a few inputs. A failed test shows a bug. A passed test shows nothing about the inputs that you did not try. A proof covers all inputs at once, and it explains why the algorithm works.

Most of the work in a proof is about loops and recursion. For a loop you find a fact that stays true at each step, and you show that this fact gives the right output when the loop ends. You also show that the loop does end.

The idea

Let $X$ be the set of inputs and $Y$ the set of outputs. A specification is a pair of predicates: a precondition $P(x)$ on inputs and a postcondition $Q(x, y)$ on an input and an output. An algorithm $A$ is correct for $(P, Q)$ when

The statement has two parts. The part "$A$ stops on $x$" is termination. The part "$Q(x, A(x))$ whenever $A$ stops" is partial correctness. A proof of each part is a different task, with different tools. Partial correctness uses loop invariants, or more generally Floyd's inductive assertions and Hoare triples. Termination uses a variant function: a quantity with values in a well-founded set, usually a non-negative integer, that drops strictly at each step. See termination proof.

For a recursive algorithm, partial correctness is proved by strong induction on a measure of the input that has no infinite decreasing sequence, for example its size. The induction hypothesis is that every recursive call on a smaller input meets the specification. The base cases are checked directly. Termination follows because every call is on a strictly smaller measure. For example, merge sort is correct on all arrays of length $n$ by strong induction on $n$.

The statement says nothing about inputs outside $P$. The algorithm may stop, fail or loop on them. This is why the precondition is part of the specification.

No algorithm decides, for every program and every specification, whether the program is totally correct (this follows from Rice's theorem). So each proof is built for its own algorithm. For a randomized algorithm the claim changes. A Monte Carlo algorithm is correct with probability at least $1 - \delta$ for a stated $\delta$. A Las Vegas algorithm is always correct, and its running time is random.

Testing and proof answer different questions. A test checks the formula above for one chosen $x$. If $A$ gives a wrong output on that $x$, the test finds a counterexample. If $A$ gives a right output, the formula is still open for every other $x$. A proof covers all $x \in X$ with $P(x)$. A proof is also a proof about a model: it uses mathematical integers, and a program on a real machine can differ from the model, for example through integer overflow.

Examples

The running example of this group of pages is integer square root. The specification is: the input is an integer $n \ge 0$, and the output is the integer $r$ with $r^2 \le n < (r+1)^2$. For each $n \ge 0$ exactly one such $r$ exists, namely $\lfloor \sqrt n \rfloor$. The algorithm is a binary search on the answer, see also integer square root.

1. ISQRT(n) ▷ n is an integer with n ≥ 0
2. 1lo ← 0
3. 2hi ← n + 1
4. 3while hi − lo > 1 do
5. 4mid ← lo + ⌊(hi − lo) / 2⌋
6. 5if mid · mid ≤ n then lo ← mid
7. 6else hi ← mid
8. 7r ← lo ▷ r is the result

Why it is correct. The loop invariant is $I$: $0 \le lo < hi$ and $lo^2 \le n < hi^2$.

1. Start. After L1 and L2, $lo = 0$ and $hi = n + 1$. Then $0 < n + 1$, and $0 \le n < (n+1)^2$ because $(n+1)^2 = n^2 + 2n + 1 > n$ for $n \ge 0$. So $I$ holds.
2. Step. Assume $I$ and $hi - lo > 1$. Put $g = hi - lo \ge 2$. Then $mid - lo = \lfloor g/2 \rfloor \ge 1$ and $hi - mid = g - \lfloor g/2 \rfloor \ge 1$, so $lo < mid < hi$. If $mid^2 \le n$, the new pair $(mid, hi)$ satisfies $I$. Otherwise $n < mid^2$, and the new pair $(lo, mid)$ satisfies $I$.
3. End. When the loop stops, $hi - lo \le 1$. With $lo < hi$ this gives $hi = lo + 1$. Then $I$ says $lo^2 \le n < (lo+1)^2$, and L7 sets $r = lo$. This is the postcondition.
4. Termination. The new gap is $hi - mid = g - \lfloor g/2 \rfloor$ or $mid - lo = \lfloor g/2 \rfloor$. Both are at most $g - 1$ when $g \ge 2$. So the integer $hi - lo$ drops by at least 1 at each step, and it stays at least 1. The loop runs a finite number of times.

For $n = 10$ the loop runs four times:

step	lo	hi	hi − lo	mid	mid² ≤ 10
1	0	11	11	5	no
2	0	5	5	2	yes
3	2	5	3	3	yes
4	3	5	2	4	no

After step 4 the pair is $(3, 4)$, so $r = 3$, and $3^2 = 9 \le 10 < 16 = 4^2$.

A bug that tests can miss. Start with $hi \leftarrow n$ instead of $n + 1$. The invariant now fails at the start for $n = 1$, because $1 < 1^2$ is false. For $n = 1$ the loop does not run, and the result is $0$, but the right value is $1$. For every $n$ other than 1 the buggy program returns the right value, because $n < n^2$ once $n \ge 2$. So a test set of thousands of inputs that leaves out $n = 1$ passes. A proof attempt fails at once in the start step, for $n = 0$ and for $n = 1$, and this points straight to the boundary.

A specification that is too weak. Take the postcondition $r^2 \le n$ alone. The program that always returns $r = 0$ meets it, and it is useless. A specification must be strong enough to exclude every wrong answer that you care about. See postcondition.

Where it is used

Correctness proofs are the basis of the proof pages on this site. They are also the base of program verification tools, and of design by contract, where preconditions and postconditions are checked at run time as assertions. Where a proof is too costly, property-based testing and differential testing check the specification on many generated inputs. They find bugs and do not prove their absence.

References

1. Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, fourth edition, Section 2.1
2. C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM 12(10) (1969), pp. 576 to 580
3. R. W. Floyd, Assigning meanings to programs, in Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, AMS (1967), pp. 19 to 32
4. Donald E. Knuth, The Art of Computer Programming, Volume 1, third edition, Section 1.2.1