What a Proof of Correctness Actually Is

The phrase "prove a program correct" hides its most important word. Correct with respect to a specification, and the specification is a separate artefact that someone has to write.

That is not a technicality. It relocates the problem rather than removing it. A verified program is one shown to satisfy its specification, and if the specification says the wrong thing, the proof is a proof of the wrong property. Verification eliminates implementation bugs and cannot eliminate specification bugs.

What it buys in exchange is a change of quantifier. Testing establishes behaviour on the inputs tried, which is a statement about some inputs. A proof establishes behaviour for all inputs satisfying the precondition, including the ones nobody thought of.

That is the entire value proposition, and the lesson What Undecidability Costs Real Tools explains why it cannot be had automatically: Rice's theorem closes every non-trivial semantic question, so a proof needs either a restricted language or human guidance. This cursus is about the machinery that guidance operates.

C. A. R. Hoare gave the standard formalism in "An Axiomatic Basis for Computer Programming", Communications of the ACM, volume 12, issue 10, 1969, pages 576 to 580.

The unit is a triple, written {P} C {Q}, where P and Q are logical assertions about program state and C is a program fragment.

It reads: if P holds before C runs, and C terminates, then Q holds afterwards. P is the precondition, Q the postcondition.

Two details in that reading do real work.

First, the conditional on termination. This is partial correctness: it promises the right answer if you get an answer. Proving that you get one is a separate obligation, and combining the two gives total correctness. The separation is deliberate, since termination arguments are usually independent of correctness arguments.

Second, assertions describe states, not values. {x > 0} x := x + 1 {x > 1} is a claim about every state where x is positive, not about a particular x.

The framing turns a program into a relation between assertions, which is what makes it something you can reason about compositionally.

The logic assigns a rule to each way of building a program, and there are only a handful.

Assignment. The rule runs backwards, which surprises people. To make Q true after x := e, require Q with every occurrence of x replaced by e beforehand. To get {?} x := x+1 {x > 1}, substitute: x+1 > 1, that is x > 0. Working backwards from the goal is the natural direction, not forwards from the inputs.

Sequence. If {P} C1 {R} and {R} C2 {Q}, then {P} C1;C2 {Q}. The intermediate assertion R is the glue, and finding it is the work.

Conditional. Prove the postcondition on both branches, each with the branch condition added to what is known.

Consequence. A precondition may be strengthened and a postcondition weakened. This is what lets a specific proof discharge a general obligation.

Loop. The one that is not mechanical, and the subject of the next step.

Everything except the loop rule is bookkeeping. Given the assertions, a machine applies these rules without help.

A loop runs an unknown number of times, so no finite unrolling proves anything about it. The device that handles this is the loop invariant: an assertion true before the loop starts, preserved by each iteration, and therefore true when the loop exits.

The rule: if {I and B} C {I}, then {I} while B do C {I and not B}.

Read the conclusion carefully. On exit you know two things: the invariant still holds, and the loop condition has become false. The proof obligation is to choose an I strong enough that those two facts together imply what you actually wanted.

That choice is the entire difficulty. An invariant that is too weak is preserved but implies nothing useful at exit. One that is too strong is not preserved and the proof fails. The right one sits between, and finding it requires understanding why the algorithm works, not merely what it does.

This is where verification stops being mechanical, and it is a direct consequence of undecidability. Invariant inference cannot be complete, so tools guess with heuristics and hand the hard cases back. An engineer stating a good invariant is supplying exactly the information a machine provably cannot derive.

Integer division by repeated subtraction, annotated with everything a checker would need.

def divide(a, b):
    # PRE:  a >= 0 and b > 0
    q, r = 0, a
    # INVARIANT:  a == q*b + r  and  r >= 0
    while r >= b:
        q, r = q + 1, r - b
    # POST: a == q*b + r  and  0 <= r < b
    return q, r

Three obligations, and each is discharged mechanically once the invariant is written down.

Establishment. Before the loop, q = 0 and r = a, so q*b + r = a, and r = a >= 0 by the precondition. The invariant holds.

Preservation. Assume the invariant and r >= b. After the body, the new value of q*b + r is (q+1)*b + (r-b), which expands to q*b + b + r - b, that is q*b + r, unchanged and still equal to a. And r - b >= 0 because r >= b. Preserved.

Exit. The loop ends when r < b. Combined with the invariant, that gives exactly the postcondition.

Notice the shape of the work. Verifying the three obligations is routine algebra. Producing the line a == q*b + r is the insight, and it is the statement of why the algorithm is correct.

The cycle in the middle is what replaces running the loop. Preservation is proved once, for an arbitrary iteration, and induction covers all of them. That is the step that turns an unbounded number of executions into a finite proof obligation.

The final implication is where a proof most often fails, and the failure is informative. If the invariant plus the negated condition does not give the postcondition, the invariant is too weak and needs strengthening. That is a concrete, actionable message, unlike a failing test.

One thing is missing from the diagram, deliberately. Nothing here proves the loop ends. Everything above holds vacuously for a loop that never exits.

Termination needs its own argument: a quantity that decreases on every iteration and cannot decrease forever, called a variant. Here it is r, which drops by at least b each time and is bounded below by zero. Adding that turns partial correctness into total correctness.

Hoare's rules verify a triple you propose. Edsger Dijkstra's reformulation computes one, which is what made the approach automatable.

Define wp(C, Q) as the weakest precondition: the least restrictive assertion that guarantees Q after running C. Then {P} C {Q} holds exactly when P implies wp(C, Q).

The advantage is that wp is computed by pushing the postcondition backwards through the program, mechanically, one construct at a time. Assignment substitutes, sequence composes, conditionals split.

The output is a single logical formula, the verification condition, whose truth is equivalent to the program being correct. Program reasoning has become formula proving, and that formula can be handed to an automated solver.

This is the architecture of every modern verification tool. The front end computes verification conditions from annotated source; a solver discharges them; anything it cannot do returns to the engineer.

Loops interrupt the mechanical part, because wp through a loop needs the invariant, which is exactly the thing that cannot be computed. So the division of labour is precise: humans supply invariants, machines do everything else.

The logic as presented assumes a simple world, and each simplification corresponds to a real extension.

Aliasing. The assignment rule substitutes syntactically, which is only sound if distinct names denote distinct locations. With pointers, writing through one name can change what another sees, and the rule breaks. Separation logic extends the framework to reason about disjoint regions of the heap, and it is what makes verifying pointer-manipulating code tractable.

Concurrency. Assertions describe the state between statements, and with another thread running there is no such quiet moment. Concurrent reasoning needs rules about interference, and it is substantially harder.

The environment. A proof covers the program, not the compiler, the operating system, the hardware, or the assumption that memory holds its contents. Everything outside is the trusted computing base, believed rather than proved.

The specification. Still the deepest limit. A proof shows the code matches the spec, and offers nothing about whether the spec matches the intent.

That last point is where the next lesson starts, because one tradition attacks it directly: rather than writing a program and proving it meets a specification, make the specification a type that only correct programs can have.