What Program Correctness Means

Ask an engineer whether their code works and the honest answer is usually "it passes the tests." But a test is a single experiment: you fed the program one input and liked what came out. Pass a thousand such experiments and you have learned that the program is right on those thousand inputs — and precisely nothing about the uncountably many you did not try. The gap between "seems to work" and is correct is not a matter of diligence; it is a matter of kind. Correctness is a claim about all inputs at once, and no finite pile of examples can establish it.

In 1972 Edsger Dijkstra put the point in a sentence that every serious programmer eventually has tattooed on their conscience: "Program testing can be used to show the presence of bugs, but never to show their absence." This page is about what the alternative — a genuine notion of correctness — actually requires. The short version: correctness is not a property a program has on its own. It is a relation between a program and a specification, and you cannot even ask whether code is correct until you have written the specification down.

Correct means "meets its specification"

A specification says what the program is supposed to do, in terms of the relationship between its inputs and its outputs — deliberately saying nothing about how. The implementation is the "how." A program is correct exactly when, for every input the specification admits, the implementation produces an output the specification permits. Correctness is therefore always relative to a spec: the very same code is "correct" against a weak spec and "buggy" against a strong one. There is no such thing as absolute, spec-free correctness — "does what I meant" is not a checkable claim until "what I meant" is written down as predicate-logic assertions about the variables.

The cleanest form of a specification is a pair: an assumption about the input (the precondition) and a requirement on the output (the postcondition). For an integer square root, for instance:

\underbrace{n \ge 0}_{\text{precondition}} \quad\longrightarrow\quad \underbrace{r^2 \le n \;\wedge\; (r+1)^2 > n}_{\text{postcondition}}

Notice that the postcondition pins down the answer without hinting at an algorithm — you could satisfy it by binary search, by Newton's method, or by a lookup table, and all three would be "correct" because correctness only cares about the input–output relation. Splitting what from how is the single most important move in the whole subject; we make it formal on the next page, specifications with pre- and postconditions.

Partial vs total correctness

There are two grades of the claim, and the difference is termination.

Partial correctness: if the program terminates on an input satisfying the precondition, then its result satisfies the postcondition. It makes no promise that the program stops at all — a program that loops forever is vacuously partially correct, because the "if it terminates" clause is never triggered.
Total correctness: partial correctness and termination — for every input meeting the precondition the program does halt, and with a right answer. In a slogan: \text{total} = \text{partial} + \text{termination}.

The split is not pedantry. Proving the input–output relation and proving termination use completely different machinery — the first is logic about states, the second needs a variant, a quantity that strictly decreases in a well-founded order. So we routinely prove partial correctness first and add termination as a separate step. Keep the distinction sharp: a proof that a loop "computes the right thing" is silent about whether the loop ever ends.

Three families of properties

Not every requirement fits the neat input-then-output mould. A program that runs indefinitely — a server, an operating system, a controller — has behaviours that unfold over time, and its correctness is phrased over executions, not just final states. Three families are worth naming now (each gets its own page later in the course).

Functional correctness — the input–output relation of a terminating computation: "the returned array is a sorted permutation of the input." This is the classic pre/post story above.
Safety — "nothing bad ever happens": some undesirable state is never reached (no two threads in the critical section, the balance never goes negative). A safety violation always has a finite witness — a prefix of an execution where the bad thing has already occurred.
Liveness — "something good eventually happens": every request is eventually served, the program eventually terminates. Termination is itself the simplest liveness property. A liveness violation needs an infinite witness — an execution that goes on forever without the good thing.

A useful rule of thumb: safety is what invariants and assertions police; liveness is what variants and fairness arguments police. We will return to safety and liveness in depth when we reach model checking.

A subtle bug a spec would have caught

Here is a routine that returns the index of the midpoint element of a sorted array — the workhorse inside binary search. It "seems to work": test it on arrays of length 3, 7, 100, and every answer is fine.

// "Seems to work" — passes every small test. function midpoint(lo: number, hi: number): number { return (lo + hi) / 2 | 0; // integer midpoint of the range [lo, hi] }

The defect is invisible to ordinary testing because it only surfaces when lo + hi overflows the machine integer — for a 32-bit signed index that is above roughly two billion, an array size nobody puts in a unit test. This is the exact bug that lurked in the JDK's binarySearch for nine years. Now watch what happens the moment you are forced to write the specification:

// The spec forces the honest question: is lo + hi always representable? // precondition: 0 <= lo <= hi // postcondition: result === lo + floor((hi - lo) / 2) // AND lo <= result <= hi (result is a valid in-range index) function midpoint(lo: number, hi: number): number { return lo + ((hi - lo) >> 1); // never forms the oversized sum lo + hi }

The postcondition lo \le \mathit{result} \le hi is a promise the buggy version cannot keep for large indices: when lo+hi wraps around it goes negative, and a negative "index" is out of range. Writing the spec did not just document the code — it dragged the hidden assumption ("lo+hi fits in an int") into the open, where it fails a proof obligation instead of a customer. That is the whole value proposition of correctness: the discipline of stating the spec surfaces the very cases testing skips.

Because proofs and tests fail in different directions, and you want both. A proof establishes the program matches the specification — but if the specification is itself wrong (you proved the wrong theorem), the proof is impeccable and the program still does the wrong thing. Testing is a cheap, empirical sanity check on the whole stack, spec included: run it, look at reality, catch the mismatch a formal argument silently propagated. Dijkstra's point is not "never test"; it is "testing has a ceiling — it can refute correctness but never confirm it, so do not mistake a green test suite for a guarantee." The mature stance is a layered one: types rule out whole classes of error at compile time, proofs establish the input–output relation, and tests keep the specification and the world honest.

The commonest confusion is to hear "partial correctness" and think it means "correct on part of the inputs" — as in "it works for most cases." It means no such thing. Partial refers to the termination clause being dropped, not to the input space being sampled: a partially correct program is right on every admissible input on which it halts. Conversely, "it passed all 500 tests" is not even partial correctness — it is a statement about 500 inputs, whereas partial correctness quantifies over all of them. Two different words, two different scopes: "partial" weakens the promise about stopping; a test suite weakens the promise about coverage. Never let one stand in for the other.