Correctness by Construction

There are two ways to end up with a correct program. The usual one: write the code, then try to prove (or test) that it works — verify after the fact. Dijkstra and David Gries championed the other, more radical one: derive the program from its specification, so that it is correct because of how it was built, not checked for correctness afterward. When the proof and the code grow together, line by line, "does it work?" stops being a question you ask at the end — it is answered as you go.

This is correctness by construction (or programming as a formal derivation): the subject of Gries' The Science of Programming. You start from the postcondition and a chosen invariant, and each program line is forced by a proof obligation. Guesswork shrinks; the code almost writes itself.

The philosophy: let the proof drive the code

In verify-after, the invariant is reverse-engineered from finished code — often the hardest part, because you are guessing what the author must have had in mind. In construction, you turn that around: you choose the invariant first, as a design decision, and then the loop guard, the initialisation, and the loop body are each derived to satisfy specific obligations. The invariant is not discovered at the end; it is the seed at the beginning.

To build a loop that establishes postcondition Q, pick an invariant I and then let the pieces fall out:

Four obligations, four pieces of program. Get the invariant right and the rest is bookkeeping — the exact opposite of staring at a blank editor wondering how to begin.

The key heuristic: replace a constant by a variable

Where does the invariant come from? The workhorse trick, due to Gries, is "replace a constant by a variable". Take the postcondition, find a constant in it, and generalise that constant into a fresh variable. The postcondition is the special case where the variable equals the constant — so the invariant is a weakened postcondition, describing partial progress.

Concretely: the goal "s is the sum of all n elements" has the constant n. Replace it with i to get the invariant "s is the sum of the first i elements." The whole loop now derives itself.

A full derivation: summing an array

Specification: given array A of length n \ge 0, establish Q \equiv s = \sum_{k=0}^{n-1} A[k]. Watch each line be forced, not invented.

Stage 1 — invent the invariant. Replace the constant n in Q by a variable i:

Invariant I: s = sum of A[0 .. i-1] AND 0 <= i <= n

Stage 2 — derive the guard. We need I \wedge \neg b \Rightarrow Q. Since I with i = n is Q, choose \neg b \equiv (i = n), i.e. the guard is i \ne n, or (with i \le n) simply i < n:

while (i < n) { ??? }

Stage 3 — derive the initialisation. Make I true cheaply. The empty sum is 0, at i = 0:

s := 0; i := 0; // I holds: s = sum of A[0..-1] = 0, and 0 <= 0 <= n while (i < n) { ??? }

Stage 4 — derive the body. Two forces act. To make progress and guarantee termination, decrease the variant V = n - i — so increment i. But i := i + 1 alone breaks I: now s is short by the element A[i]. To restore I we must add A[i] to s before bumping i. The body is forced:

let s = 0, i = 0; // Invariant I: s === sum of A[0..i-1] and 0 <= i <= n; Variant V = n - i while (i < n) { s = s + A[i]; // forced: restores I for the new i i = i + 1; // forced: decreases V = n - i, makes progress } // Here !b gives i = n, so with I: s === sum of A[0..n-1] = Q. Done.

Not one line was a free choice. The invariant came from a mechanical heuristic; the guard, the init, and both body statements were each dictated by an obligation (imply Q, establish I, restore I, decrease V). The program is correct by construction, and the proof is already written — it is the derivation.

The same recipe: linear search

The method is not a one-off. Specify: find the least index i with A[i] = x (assume x is present). Replace the constant "answer index" with a running i; the invariant becomes "x is not among A[0..i-1]." The guard is "A[i] \ne x" (keep going while not found); the init is i := 0 (nothing scanned yet); the body i := i + 1 is forced to both restore the invariant and shrink the variant V = n - i.

let i = 0; // Invariant: x is not in A[0..i-1]; Variant V = n - i while (A[i] !== x) { i = i + 1; // forced: restores "not found yet", decreases n - i } // On exit A[i] === x, and x was in none of A[0..i-1] — so i is the LEAST such index.

Same four stages, a different specification, and again every line is a forced move. That reproducibility is the point: correctness by construction turns programming from inspiration into a calculational discipline.

For a three-line sum, sure — the derivation looks like heavy machinery for an obvious loop. The payoff appears exactly where intuition fails: subtle loops with off-by-one traps, tricky boundary conditions, interleaved updates that must happen in a particular order (like adding A[i] before incrementing i, not after). In those cases the derivation tells you the order, the initial values, and the exact guard, instead of leaving you to debug them. Dijkstra's slogan was that a discipline of programming lets you write code that is correct the first time — and even when you do write first and prove later, the habit of asking "what invariant is this loop maintaining, and what variant is it decreasing?" is the single most powerful tool for getting loops right.

The commonest construction bug is getting the body's statement order wrong. In the array sum, s := s + A[i] must come before i := i + 1: the invariant says s holds the sum of A[0..i-1], so you add the element at the current i (which is about to become the last one included) and only then advance. Swap them and you add A[i+1], skip A[0], and read past the end — a classic off-by-one. The derivation is not being pedantic: the obligation "the body re-establishes I" has exactly one correct order, and following the proof hands it to you. Whenever your loop is off by one, suspect the body order or the initial value of the invariant's variable — the derivation pins down both.