Total Correctness

Put the two halves together and you get the thing you actually want. A program is partially correct if, should it terminate, its answer satisfies the spec — proved with an invariant. It terminates if it always halts — proved with a variant. Neither alone is enough: a partially-correct program might loop forever and never answer; a terminating program might halt with garbage. Total correctness is the conjunction of both.

\text{total correctness} \;=\; \text{partial correctness} \;+\; \text{termination.}

Written [P]\, C\, [Q] (square brackets, to distinguish it from the partial triple \{P\}\,C\,\{Q\}): "starting from any state satisfying P, C is guaranteed to halt in a state satisfying Q."

The total-correctness while rule

For loop-free code, partial and total correctness coincide — nothing can diverge. All the action is at the loop, and the total rule is the partial loop rule with a variant welded on. You supply two witnesses: an invariant I (for the answer) and a variant V (for halting).

To conclude [I]\;\texttt{while } b \texttt{ do } C\;[I \wedge \neg b], discharge:

Then the loop halts and establishes I \wedge \neg b. The first bullet gives you the right answer if it stops; the last two guarantee it stops.

Everything is checked together and locally — you never unroll the loop, never count iterations by hand. Find I and V, discharge three obligations about a single pass of the body, and the loop is totally correct for all inputs at once.

Why wp already bakes in termination

There is a slick way to see total correctness: it is exactly what weakest preconditions compute. Recall the two transformers:

So Dijkstra's calculus does not treat termination as an add-on. The moment you compute \operatorname{wp} rather than \operatorname{wlp}, you are asking for total correctness — the variant reappears as the ingredient needed to give the loop's \operatorname{wp} a finite, well-founded meaning.

A full total-correctness proof

Let us prove a summation loop totally correct. It should leave s = \sum_{k=0}^{n-1} A[k] for an array A of length n \ge 0.

// Pre: n >= 0 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]; i = i + 1; } // Post: s === sum of A[0..n-1]

Invariance. Before the loop, i = 0 and s = 0 — the empty sum — so I holds. If I and i < n hold, then adding A[i] to s and incrementing i re-establishes s = \sum_{k=0}^{i-1} A[k] with the new i, and 0 \le i \le n is maintained. So \{I \wedge i < n\}\;\text{body}\;\{I\}.

Termination. Take V = n - i. While the guard i < n holds, V = n - i > 0 \ge 0, so it is bounded below. The body increments i by 1, so V drops by exactly 1 each pass — strictly decreasing. Three obligations discharged.

Exit. On termination the guard fails, giving i \ge n; with the invariant's i \le n we get i = n, so s = \sum_{k=0}^{n-1} A[k] — the postcondition. The loop is totally correct.

Trace it for A = [4, 2, 7] (n = 3) and watch both the invariant hold and the variant fall in lockstep, all the way to the floor:

point i s invariant s = \sum_{k \lt i} A[k] variant V = n - i
before loop00✓ (empty sum)3
after pass 114✓ (4)2
after pass 226✓ (4+2)1
after pass 3313✓ (4+2+7)0 — guard fails, exit

The invariant column is always ✓ (never violated — that is what "invariant" means); the variant column marches 3, 2, 1, 0 straight down to the floor, and the instant it can go no lower the guard fails and we leave with the answer. Partial correctness rides the first column; termination rides the last.

An invariant is, by design, a property that does not change — it says nothing about progress. The loop \texttt{while } \texttt{true} \texttt{ do skip} keeps the invariant "\texttt{true}" perfectly, iteration after iteration, forever. Every non-terminating loop preserves some invariant; preservation and progress are orthogonal. That is the whole reason total correctness needs a second, independent witness — the variant — whose job is precisely to measure decreasing progress toward a floor. Invariant = "still right"; variant = "getting closer to done." You cannot squeeze the second out of the first, which is why Hoare's original loop rule proves only partial correctness and the total rule adds a whole extra ingredient.

Two failure modes sink total-correctness proofs. (1) Momentary dips don't count. The variant may wobble up mid-body as long as its value at the end of the body is strictly below its value at the start — the obligation is \{V = k\}\,\text{body}\,\{V < k\}, comparing entry to exit, not every instruction. (2) Bounded-below is required only while the guard holds. You must show I \wedge b \Rightarrow V \ge 0; it is fine for V to be -1 after the loop exits (indeed V = n - i = 0 at exit above, and one more decrement would go negative — but the guard has already stopped us). Forgetting to tie the bound to the guard, or checking the decrease at the wrong granularity, produces "proofs" of loops that never stop.