← Back to System Internals

The Iterative Command — Loops, Invariants & Bounds

The centrepiece of Gries’ calculus: how the guarded do…od loop is given meaning, why its weakest precondition has no closed form, and how a loop invariant plus a bound function let you prove — and design — a loop that is totally correct.

Every other command in Gries’ tiny language has a weakest precondition you can write down and compute directly. The loop does not. A loop can iterate any number of times depending on its data, so its wp is a fixed point over unbounded repetition — you cannot evaluate it in your head or on paper. Gries’ answer is to stop trying. Instead of computing the loop’s wp, you prove the loop correct against a specification using two objects you invent yourself: a loop invariant that captures what stays true across iterations, and a bound function that forces termination. This page is the heart of the method — the same invariant that proves a loop is what lets you write it in the first place.

The guarded loop

The iterative command is Dijkstra’s guarded repetition. In its simplest single-guard form it repeats one body while a condition holds:

do B → S od     # repeat S as long as B is true; stop when ¬B

The general form has several guarded commands, exactly like if…fi but repeated:

do B1 → S1
[] B2 → S2
   …
[] Bn → Sn
od

Semantics. On each pass the loop looks at all the guards. If at least one is true, it chooses one true guard (nondeterministically, if several are true) and executes its body; then it repeats. The loop terminates only when all guards are false. The crucial payoff is what you know at that moment: on normal termination the loop has established ¬B for the single-guard form, or ¬B1 ∧ ¬B2 ∧ … ∧ ¬Bn for the general form. Unlike if…fi, an empty set of true guards does not abort the loop — it is precisely how the loop ends normally.

Why wp has no closed form

For every other command, wp(S, R) is a finite formula you can build mechanically. The loop breaks this, because the number of iterations is not fixed — it depends on the starting state. Formally, wp(DO, R) is defined as a limit over “terminates in at most k iterations” predicates. Write IF for the selection command with the loop’s guards and bodies. Then:

Read it informally. H0(R) says “the loop is already done — the guard is false and R already holds, so zero iterations suffice.” Hk(R) says “either the loop finishes in at most k−1 more iterations after one step, or it was already done.” The full wp is then: “there exists some number of iterations k after which the loop has terminated in a state satisfying R.” That existential over an unbounded k is the fixed point — and there is no way to collapse it into a single computable expression for an arbitrary loop.

The loop invariant P

The invariant P is a predicate that is true before the loop begins and true again after every complete iteration of the body. It may be temporarily broken in the middle of the body, but the body must always restore it before the next guard test. Intuitively, P asserts that “the work done so far is consistent and correct” — it is the loop’s running promise about its own partial results.

That exit condition, P ∧ ¬B, is the entire reason the invariant is worth inventing. The invariant captures the correct-so-far part; the negated guard captures the done part; together they must add up to the postcondition you want. In a real sense the invariant is the meaning of the loop: it says what the loop is doing, independent of how many times it runs. A loop without a stated invariant is a loop nobody — including its author — can be sure is correct.

The bound function t

The invariant guarantees that if the loop stops, it stops in a good state — but it says nothing about whether the loop stops at all. Termination is the job of the bound function t: an integer-valued expression over the program variables with two properties.

The termination argument is then a simple appeal to the well-ordering of the integers: t starts at some finite value, drops by at least one each pass, and cannot fall below zero while the loop runs. An integer cannot decrease forever while staying positive, so after finitely many iterations the guard must become false and the loop halts. The bound function is the loop’s clock, counting down to a guaranteed stop.

The five-part checklist for total correctness

To prove that {Q} init; do B → S od {R} is totally correct — it terminates and establishes R — using invariant P and bound function t, discharge all five obligations below. Passing every one is sufficient; there is nothing left to check.

Conditions 1–3 establish partial correctness (correct answer if it halts); conditions 4–5 add termination. Together they give total correctness.

Reading the checklist as a design tool

The five conditions are usually presented as a proof burden, but Gries’ deeper point is that they are a design procedure. Read the roles they play:

• Conditions 1–3 pin down the frame. Condition 3 (P ∧ ¬B ⇒ R) forces the guard to be exactly what is missing between the invariant and the postcondition — so choosing P essentially determines B. Condition 1 tells you what the initialisation must accomplish (make P true cheaply). Condition 3 also confirms that the postcondition really is reachable this way.
• Conditions 4–5 constrain the body to make progress. Once P and B are fixed, the body S is whatever preserves P (condition 2) while strictly shrinking a positive bound (conditions 4–5). That is a tight box — often only one reasonable body fits.

The order matters: the invariant is chosen first, and everything else follows. You do not write a loop and then hunt for its invariant; you decide what must stay true, and the guard, the initialisation, the body, and the termination argument fall out of it almost mechanically. That inversion — invariant leads, code follows — is the whole transition into program development, covered in inventing invariants & developing loops.

Fully worked example: integer division

Compute the quotient q and remainder r of a ÷ b using only repeated subtraction. This is the canonical Gries derivation, worked here through every one of the five checklist conditions.

# Specification
# pre  Q:  a ≥ 0  and  b > 0
# post R:  a = q*b + r   and   0 ≤ r < b

The design choices, made invariant-first:

The invariant is the postcondition with its hardest conjunct, r < b, deleted; the guard is exactly that deleted conjunct negated. Now walk the checklist.

Condition 1 — Q ⇒ wp(init, P) (init establishes P). Compute wp("q:=0; r:=a", a = q*b + r ∧ 0 ≤ r) by backward substitution: replace q by 0 and r by a, giving a = 0*b + a ∧ 0 ≤ a, i.e. a = a ∧ a ≥ 0. The first term is trivially true; the second is exactly the precondition a ≥ 0. So Q ⇒ wp(init, P). ✓

Condition 2 — {P ∧ B} S {P} (body preserves P). Assume a = q*b + r, 0 ≤ r, and r ≥ b. After the body sets r to r−b and q to q+1, check the invariant on the new values:

so a = q*b + r still holds; and since r ≥ b we have r − b ≥ 0, so 0 ≤ r still holds. The invariant is preserved. ✓

Condition 3 — P ∧ ¬B ⇒ R (exit gives the result). On exit the guard is false: ¬(r ≥ b), i.e. r < b. Combined with the invariant a = q*b + r ∧ 0 ≤ r, we get a = q*b + r ∧ 0 ≤ r < b — exactly the postcondition R. ✓

Condition 4 — P ∧ B ⇒ t > 0 (bound positive while looping). The bound is t = r. While looping, the guard B gives r ≥ b, and the precondition established b > 0, so r ≥ b > 0, hence t = r > 0. ✓

Condition 5 — {P ∧ B} t0 := t; S {t < t0} (bound strictly decreases). Snapshot t0 = r before the body. The body sets r to r − b, and since b > 0 we have r − b < r = t0. So the new bound t = r − b satisfies t < t0. The loop must terminate. ✓

All five hold, so the program below is totally correct by construction.

# {a ≥ 0 and b > 0}
q := 0 ;  r := a ;
# invariant P: a = q*b + r and 0 ≤ r
# bound     t: r
do r ≥ b →
     r := r - b ;
     q := q + 1
od
# {a = q*b + r and 0 ≤ r < b}

Every line was forced by the specification and the chosen invariant: nothing was guessed and later patched by testing.

Partial vs total correctness

It is worth naming exactly what each half of the checklist buys you. Conditions 1–3 alone establish partial correctness: if the loop terminates, its result satisfies R. They say nothing about whether it terminates — a loop that runs forever is vacuously partially correct, because it never produces a wrong answer, it simply never produces one.

Dropping the bound function t throws away conditions 4 and 5, leaving only partial correctness. Gries insists on total correctness — a program that might not terminate is not a program you have proven anything useful about. The bound function is not optional bookkeeping; it is what turns “correct if it stops” into “correct.”

Summary