← Back to System Internals

Developing Programs — Goal-Oriented Construction & Inventing Invariants

The practical payoff of Gries’ calculus: how to let a specification drive the code, and — the part everyone finds hard — how to actually invent a loop invariant instead of guessing one.

The first half of The Science of Programming builds machinery: predicates, weakest preconditions, the five commands and their wp. This page is about spending that machinery. Given a precondition Q and a postcondition R, how do you develop a program — not verify one after the fact, but grow it so that it is correct the moment it is finished? Gries’ answer is a small kit of refinement steps and, above all, four concrete strategies for manufacturing a loop invariant out of the postcondition. That invariant, once you have it, hands you the guard, the initialisation, and the body almost for free.

Programming as a goal-oriented activity

Programming, in Gries’ treatment, is not typing statements and watching what happens. It is a goal-oriented activity: you begin with two predicates — the precondition Q that you may assume, and the postcondition R that you must guarantee — and you let the goal R drive the construction. Because wp is computed by pushing a postcondition backward through a command, the natural direction of design is also backward: start at the result you want and ask what must be true just before it.

Development is a sequence of refinement steps. At each step you replace a piece of “yet to be written” specification with a construct, and you keep an obligation attached to it: whatever you write must, together with what precedes it, satisfy Q ⇒ wp(S, R). Nothing is added on a hunch; each refinement is justified by the proof obligation it discharges. When the last hole is filled, the program is finished and, simultaneously, proven.

# start typing, keep R only in your head
i = 0
s = 0
while i < n:      # why i < n? why start at 0?
    s += b[i]     # the reasons live nowhere
    i += 1
# correct? off by one? empty array?
# you learn the answer from a failing test

# goal R: s = (Sum j: 0≤j<n: b[j])
# weaken R to an invariant P (below)
# P then FORCES:
#   init  s,i := 0,0   (makes P true)
#   guard i =/= n      (P and not-B => R)
#   body  s,i := s+b[i], i+1  (keeps P)
# the reasons ARE the derivation

Gries’ recurring slogan for this discipline: “the proof usually leads the program.” You do not write code and then look for a proof; you carry the proof obligation forward and let it dictate the next construct. See predicate & quantifier notation for the algebra these obligations are written in, and loop mechanics for the wp rules the steps rely on.

The command that establishes R

Every refinement step reduces to one question: “what is the last thing that must be true, and which construct’s wp matches it?” You look at the shape of R (and what already holds) and choose the construct whose weakest precondition, applied to R, is something you can establish.

The heuristic is mechanical and honest: hold R up against the four wp shapes and take the first that fits what you can prove from Q. When R requires accumulating a result over a data structure — a sum, a search, a maximum — no single assignment or finite case-split reaches it, and you are pushed to a loop. That is the interesting case, and the rest of this page is about it.

Developing a loop from an invariant

Once you know R needs a loop, do not start with the body. Gries’ master recipe builds the loop outward from an invariant, in a fixed order. Everything else follows.

1. Find a candidate invariant P — usually by weakening R (drop or generalise part of it, per the four strategies below). P is what stays true across every iteration: “the work done so far is consistent.”
2. Choose the guard B so that P ∧ ¬B ⇒ R. The guard is exactly the gap between the invariant and the full result — when the loop stops, P plus a false guard must give you R.
3. Choose init to establish P — pick the initialisation that makes P trivially true (usually the empty / zero-work case), so that Q ⇒ wp(init, P).
4. Choose the body to reduce a bound t (an integer, ≥ 0 while looping) while re-establishing P, i.e. {P ∧ B} S {P} and t strictly decreases.

Read that order carefully: the invariant is decided first and the body last. Beginners do the opposite — they write a body and hope an invariant exists — which is why their loops have off-by-one and boundary bugs. Full mechanics of the five wp obligations behind these steps are on the iteration page.

Four strategies for finding an invariant

This is the heart of program development, and the part with no mechanical shortcut — but there are reliable strategies. Almost every invariant you will ever need comes from one of four ways of weakening the postcondition so that it becomes something achievable early and maintainable throughout.

Strategy 1 — Deleting a conjunct

The workhorse. Integer division: post a = q*b + r ∧ 0 ≤ r ∧ r < b. Drop the hardest conjunct, r < b. What remains is the invariant, and the negation of the dropped conjunct is the guard.

# post R: a = q*b + r and 0≤r and r<b
# drop  r<b  ->  it becomes the guard
# invariant P: a = q*b + r  and  0 ≤ r
# guard     B: r ≥ b       (= not(r<b))
# init:  q,r := 0,a   (a=0*b+a, 0≤a)  P true
# body:  r,q := r-b, q+1   (bound t = r)
do r ≥ b → r := r - b ;  q := q + 1 od
# P and not-B  =>  a=q*b+r and 0≤r<b = R

Strategy 2 — Replacing a constant by a variable

Summation: post s = (∑ j: 0 ≤ j < n: b[j]). The constant n is the upper bound of the range. Replace it with a fresh variable i and require the partial result over 0..i. The loop grows i until it reaches n.

# post R: s = (Sum j: 0≤j<n: b[j])
# replace n by fresh i:
# invariant P: s = (Sum j: 0≤j<i: b[j])
#              and 0 ≤ i ≤ n
# guard     B: i =/= n
# init:  s,i := 0,0   (empty sum, i=0)  P true
# body:  s,i := s+b[i], i+1  (bound t = n-i)
do i ≠ n → s := s + b[i] ;  i := i + 1 od
# P and i=n  =>  s = (Sum j:0≤j<n: b[j]) = R

Strategy 3 — Enlarging the range of a variable

Let a variable roam over a wider set than its final answer, then shrink that set. Binary search keeps the target inside a half-open interval [lo, hi) and halves it each step; the invariant states where the answer must be.

# find where x sits in sorted b[0..n-1]
# invariant P: 0 ≤ lo ≤ hi ≤ n
#   and b[lo-1] ≤ x < b[hi]  (sentinel form)
# guard     B: lo + 1 =/= hi
# init:  lo,hi := 0,n   (widest interval)  P true
# body:  narrow via midpoint (bound t = hi-lo)
do lo+1 ≠ hi →
     m := (lo + hi) / 2 ;
     if b[m] ≤ x → lo := m
     [] b[m] >  x → hi := m
     fi
od
# interval shrinks to pin x's position

Strategy 4 — Combining pre- and post-conditions

Sometimes the invariant is simply the conjunction of what Q guarantees and the partial R being built — the properties that must hold on every iteration, not just at the ends. Linear search for the first occurrence of x combines “x is present” (from Q) with “x not seen yet” (partial R).

# pre  Q: x occurs in b[0..n-1]
# post R: 0≤i<n and b[i]=x and x not in b[0..i-1]
# invariant P (conjoin both):
#   0 ≤ i ≤ n
#   and x not in b[0..i-1]     (partial R)
#   and x occurs in b[i..n-1]  (from Q, kept alive)
# guard  B: b[i] =/= x     bound t: n - i
# init:  i := 0            (empty prefix)  P true
do b[i] ≠ x → i := i + 1 od
# P keeps x in b[i..n-1], so i never runs off n

Note how, in strategy 4, the conjunct pulled from Q (“x occurs in b[i..n-1]”) is precisely what guarantees the array access b[i] is always in bounds. The invariant is carrying the safety argument, not just the result.

Checklist-driven completion

Once P and B are chosen, you do not guess the rest — you mechanically discharge the five loop conditions (the full list lives on the iteration page), and each condition either checks out or tells you exactly what is missing.

The powerful part: a failing condition tells you precisely what to add. Suppose in the linear search you weaken the precondition so x is not guaranteed present. Then condition 2, {P ∧ B} i := i+1 {P}, breaks: the body evaluates b[i] in the guard, but P no longer promises i < n, so the access may be out of bounds. The fix is not a patch — the failed obligation dictates it: strengthen the guard with a bounds check, using conditional conjunction so the array is only touched when safe.

# P no longer guarantees i < n
do b[i] ≠ x → i := i + 1 od
# when x absent, i reaches n and
# b[i] indexes out of bounds -> abort
# condition 2 fails: it tells you the fix

# add i<n to the guard (cand = short-circuit)
# invariant relaxed to: 0 ≤ i ≤ n
do i < n cand b[i] ≠ x → i := i + 1 od
# b[i] evaluated only when i<n  -> safe
# on exit: i=n (absent) or b[i]=x (found)

This is the sense in which the proof does the design. You are never left wondering whether an edge case is handled; an unmet obligation names the exact conjunct you forgot.

The Fundamental Invariance Theorem

The formal backbone under conditions 1–3 is what Gries calls the Fundamental Invariance Theorem. Stated for partial correctness:

In words: if each execution of the body, starting from a state where P and the guard B both hold, ends in a state where P holds again, then the whole loop — however many times it iterates — preserves P, and on termination adds ¬B. That is exactly why P is called an invariant: the loop cannot falsify it.

The justification is induction over the number of iterations. Base case: zero iterations — P holds by assumption on entry. Inductive step: assume P holds after k iterations; if the loop runs once more then B was true, so {P ∧ B} S {P} gives P after iteration k+1. Hence P holds after every iteration; when the loop stops, the guard is false, so P ∧ ¬B. Add a bound function t (conditions 4–5) and induction on iterations becomes well-founded — the loop cannot iterate forever — upgrading partial correctness to total correctness. This theorem is the license for the whole develop-from-an-invariant method: prove one local fact about the body, get a global fact about the loop.

Summary