← Back to System Internals

The Science of Programming — Gries, Distilled

A working reference to David Gries’ classic on proving programs correct — predicate logic, weakest preconditions, and the discipline of developing a program and its proof hand in hand rather than coding first and testing later.

David Gries’ The Science of Programming (1981) makes one radical claim: a correct program and its correctness proof should grow together. You do not write code and then hope tests catch the bugs; you let the specification — a precondition and a postcondition — drive the code, so that the finished program is correct by construction. The mathematics behind this is Dijkstra’s calculus of weakest preconditions, and the everyday tool it hands you is the loop invariant. This guide walks the logic prelude, the semantics of a tiny language, and the program-development strategies, with worked derivations.

The central thesis

The prevailing habit — then and, honestly, now — is to write the program first and reason about it (if at all) afterward. Gries inverts this. The specification comes first as a pair of predicates, and each construct you add is chosen to satisfy the proof obligation it creates. Debugging is thereby replaced by derivation.

# write it, run it, patch what breaks
def divide(a, b):
    q = 0
    r = a
    while r >= b:
        r = r - b
        q = q + 1
    return q, r
# is it right for a=0? b>a? negatives?
# you find out from failing tests

# Start from the contract, derive the body
# pre:  a ≥ 0  and  b > 0
# post: a = q*b + r  and  0 ≤ r < b
# invariant: a = q*b + r  and  0 ≤ r
# the loop guard, init, and body all
# fall out of that invariant (see below)

Gries’ famous line captures the spirit: “A program and its proof should be developed hand in hand, with the proof usually leading the way.” Testing shows the presence of bugs, never their absence; a proof addresses the absence directly.

Part I: The logic prelude

Before any programming, the book spends real time on the mathematics you will reason in. Skipping it is why most people bounce off formal methods.

• State. A state is an assignment of values to the program’s variables — a single point in the space of all possible variable values.
• Predicate. A predicate is a boolean expression over variables; equivalently, it names the set of states in which it is true. x > 0 denotes every state where x is positive. T (true) denotes all states; F denotes none.
• Stronger / weaker. P is stronger than Q if P ⇒ Q — a stronger predicate is more restrictive (a smaller set of states). F is the strongest predicate; T is the weakest. “Weakest” will matter enormously in a moment: it means “the most permissive condition that still works.”
• Quantifiers. The book fixes a clean notation for ∀ and ∃ over ranges, plus the identities you need to manipulate them — De Morgan, distribution, range splitting — which reappear constantly when reasoning about arrays.

Part II: Weakest preconditions

The heart of the book is Dijkstra’s predicate transformer wp. For a command S and a desired postcondition R:

Read it as: “the weakest precondition under which S is guaranteed to establish R.” It is the exact, most permissive requirement on the starting state. Note the word guaranteed — wp encodes total correctness (the command must terminate), not merely partial correctness.

Hoare triples vs. wp

The Hoare triple {P} S {Q} means: if P holds and S is executed, then Q holds afterward. It relates to wp by a single implication:

So wp(S, Q) is the weakest such P — every valid precondition for reaching Q implies it. This is why deriving wp backward from the postcondition is the engine of program construction.

Healthiness properties of wp

Every well-defined command’s wp obeys four laws. They are both a sanity check and a proof toolkit.

The assignment axiom

The single most surprising rule in the book. The weakest precondition of an assignment is the postcondition with the variable textually replaced by the expression — and the substitution runs backward, which trips up everyone the first time.

# "x := 5, so afterward x = 5"
# people try to push forward and
# substitute into the PREcondition.
# That is not what the axiom says.

# Want post: x > 10 after  x := x + 1
# Wrong guess: pre is x > 10

# wp("x := x + 1", x > 10)
#   = (x > 10)[x := x + 1]
#   = (x + 1 > 10)
#   = x > 9

# So: {x > 9} x := x + 1 {x > 10}   ✓
# Substitute into the POSTcondition.

A subtlety Gries is careful about: e must be defined in the starting state (no division by zero, no array index out of bounds). The full rule carries a domain condition: wp(“x := e”, R) = domain(e) ∧ R[x := e].

The commands & their wp

The language is deliberately tiny — five constructs — because a small language means few axioms to trust. Everything reduces to these.

Composition is the key insight to internalise: to find the precondition of a sequence, push the postcondition right-to-left through the statements. You reason from the goal backward to the start — the opposite of how the machine runs, and exactly how you should design.

# {?}  t := x ;  x := y ;  y := t   {x = Y0 and y = X0}   (swap)
wp("y := t", x=Y0 ∧ y=X0)          = (x=Y0 ∧ t=X0)
wp("x := y", x=Y0 ∧ t=X0)          = (y=Y0 ∧ t=X0)
wp("t := x", y=Y0 ∧ t=X0)          = (y=Y0 ∧ x=X0)
# precondition x=X0 and y=Y0  →  the swap is proven correct

Guarded selection (IF)

Selection is Dijkstra’s guarded command: a set of guard → statement pairs. At runtime one guard whose condition is true is chosen (nondeterministically if several are), and its statement runs. If no guard is true, the command aborts — so covering all cases is a proof obligation, not an afterthought.

if B1 → S1
[] B2 → S2
[] B3 → S3
fi

Read the two halves: the first conjunct (B1 ∨ B2 ∨ B3) says at least one guard must hold — this is what forces you to handle every case. Each remaining conjunct says whichever branch is taken must establish R. The classic max-of-two, correct by covering both guards:

if x > y → m := x
[] x < y → m := y
fi
# x = y is uncovered → aborts.
# (B1 ∨ B2) is not T, so wp fails.

if x ≥ y → m := x
[] y ≥ x → m := y
fi
# x = y satisfies both; either arm
# establishes m = max(x,y). Overlap
# is fine — both give a correct R.

The loop and its invariant (DO)

The loop is where all the machinery pays off. A guarded loop repeats: while any guard is true, pick one and run its body; stop when all guards are false.

do B → S od     # repeat S while B holds; stop when ¬B

wp of a loop cannot be written as a neat closed form — it is a fixed point over unbounded iteration. So instead of computing it, you prove the loop against a specification using two inventions of your own: a loop invariant P and a bound function t.

• Invariant P: a predicate true before the loop and after every iteration. It is the “work done so far is consistent” assertion — the heart of the loop’s meaning. On exit, you know P ∧ ¬B.
• Bound function t: an integer expression, bounded below by 0 while the loop runs and strictly decreased by every iteration. It is what proves termination.

To prove {Q} init; do B → S od {R} totally correct, discharge this five-part checklist:

Developing loops from invariants

Where does the invariant come from? Gries’ most practical contribution: a small set of heuristics for manufacturing an invariant by weakening the postcondition. A good invariant is often the postcondition made reachable early — something true at the start, that the loop drives toward the full result.

The dominant one, “delete a conjunct,” is worth burning in: your postcondition is usually “the answer is computed and we’ve processed everything.” Keep the first part as the invariant, and “we’ve processed everything” becomes ¬B — the reason the loop stops.

Worked example: integer division

Compute quotient q and remainder r of a ÷ b using only subtraction. This is the canonical Gries derivation.

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

Step 1 — invent the invariant by deleting a conjunct. The postcondition is (a = q*b + r) ∧ (0 ≤ r) ∧ (r < b). Drop the hardest-to-establish conjunct, r < b. What remains is the invariant:

Step 2 — the guard is the deleted conjunct, negated. We loop while r < b is not yet true, i.e. while r ≥ b. So B: r ≥ b, and on exit P ∧ ¬B gives exactly the full postcondition (checklist #3 ✓).

Step 3 — initialise to make P trivially true. Set q := 0; r := a. Then a = 0*b + a and a ≥ 0 from the precondition, so P holds (checklist #1 ✓).

Step 4 — the body must preserve P while shrinking a bound. Take bound t = r. When r ≥ b, subtract b from r and bump q — a = q*b + r is preserved (one b moves from r into the q*b term) and r strictly drops by b > 0 (checklist #2, #4, #5 ✓).

# {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}

# before body:  a = q*b + r,  r ≥ b
# after r:=r-b, q:=q+1 :
#   (q+1)*b + (r-b)
# = q*b + b + r - b
# = q*b + r   = a          ✓ invariant held
# and r-b ≥ 0 since r ≥ b  ✓ 0 ≤ r held
# and r-b < r              ✓ bound decreased

Every line of the program was forced by the specification and the invariant. Nothing was guessed and patched.

Worked example: linear search

Find the first index i in b[0..n-1] where b[i] = x, assuming x is present. This shows the replace-a-constant / enlarge-the-range flavour.

# 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 — enlarge the range: let i range over the scanned prefix, asserting x has not been seen yet and x is still somewhere from i onward:

i := 0 ;
# invariant P (above);  bound t: n - i
do b[i] ≠ x →
     i := i + 1
od
# {b[i] = x and x not in b[0..i-1]}

# init: i=0 → prefix b[0..-1] empty,
#       x in b[0..n-1] from precond   ✓ P
# guard false: b[i] = x               ✓ post
# P says x is in b[i..n-1], so if
#   b[i] ≠ x it must be further right
#   → i+1 keeps P, and never runs off  ✓
# bound n - i drops each step > 0     ✓ halts

Notice the precondition (“x is present”) is exactly what keeps the invariant’s last conjunct alive and guarantees the loop never indexes past n-1. Drop that precondition and the derivation immediately tells you what breaks — you would need a compound guard i < n cand b[i] ≠ x. The proof is doing design work for you.

Summary