← CatZep/Engineering Guides/The Science of Programming
Seven complete derivations in the style of David Gries’ The Science of Programming — each starting from a precondition and postcondition, choosing an invariant strategy, and letting the guard, initialisation, body, and termination argument fall out of the invariant.
Student edition · understand, apply, verify
Connect array sums, division, search, maxima, power, GCD, and partitioning to their complete contracts.
What you should be able to do: Implement the derivations with integer domains, valid ranges, permutation/frame conditions, and empty-case policy.
Assumes basic programming, not formal-methods notation. This guide defines the needed notation locally. Scalar proofs use mathematical integers unless stated otherwise; finite arrays require integer valid bounds. Guarded-command notation is not Python syntax. Machine overflow, floats, exceptions, aliasing, and concurrency need additional contracts.
These are chosen derivations from specifications. A specification can admit many valid algorithms; invariants justify these choices rather than uniquely forcing every line.
{P} S {Q} for a Hoare triple, guarded commands (if…fi, do…od), and := for assignment.Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.
A precondition states required inputs/state before an operation. A postcondition states the result promised when those requirements hold and execution terminates normally. Together they make requirements testable.
Example. For sum_first(b,n), require integer 0≤n≤len(b) and numeric elements; promise the sum of b[0:n].
Boundary. State exceptions, mutation, numeric domains, and empty cases. A mathematical array range does not automatically validate a runtime input.
A predicate true after initialization and after each iteration. Together with the false exit guard it establishes the required result.
Example. While summing, preserve 0≤i≤n and s=sum(b[0:i]); add b[i] then advance i.
Boundary. An invariant alone does not prove termination. Validate array/domain bounds and establish the invariant before iteration.
A variant strictly decreases each iteration in a well-founded order. A natural-number variant cannot decrease forever while remaining nonnegative.
Example. An array scan uses n−i; repeated subtraction division uses remaining dividend.
Boundary. A positive real can halve forever. Use discrete domains or another well-founded order; nested loops need a correct combined or lexicographic bound.
Guarded selection can choose any enabled branch. Every enabled choice must preserve correctness. No enabled selection guard aborts; an iteration stops when all guards are false.
Example. Choosing max(x,y) with guards x≥y and y≥x permits either branch on equality.
Boundary. This differs from Python's first-matching if/elif. Check coverage under the precondition/invariant; do not assume fairness unless specified.
Big-O describes growth with input size under a cost model. Worst-case, expected, amortized, and output-sensitive bounds are distinct promises.
Example. Binary search is O(log n) comparisons on sorted random-access input; printing every subset needs exponential output work.
Boundary. Expected hash-table O(1) is not worst-case O(1). Include output size, recursion space, input assumptions, integer costs, and library operations.
Compute the sum of the first n elements of an array b. The canonical illustration of replace a constant by a variable.
# Specification
# pre Q: 0 ≤ n
# post R: s = (Σ j : 0 ≤ j < n : b[j])Strategy — replace a constant by a variable. The postcondition sums the fixed range 0..n. Replace the constant upper bound n by a fresh variable i, giving a family of partial sums the loop can grow toward the full one.
Guard, bound, init. The loop must run until i reaches n, so the guard is B: i ≠ n; on exit P ∧ ¬B gives i = n, i.e. exactly R. Bound t = n - i. Initialise i := 0; s := 0 so P holds with the empty sum.
# {0 ≤ n}
i := 0 ; s := 0 ;
# invariant P: s = (Σ j:0≤j<i:b[j]) and 0 ≤ i ≤ n
# bound t: n - i
do i ≠ n →
s := s + b[i] ;
i := i + 1
od
# {s = (Σ j:0≤j<n:b[j])}# before body: s = (Σ j:0≤j<i:b[j]), i ≠ n
# after s:=s+b[i], i:=i+1 :
# s' = (Σ j:0≤j<i:b[j]) + b[i]
# = (Σ j:0≤j<i+1:b[j]) (range split)
# and i' = i+1, with i≠n ⇒ i+1 ≤ n ✓ P held
# bound: (n-(i+1)) < (n-i) ✓ decreased
# t > 0 while i ≠ n (since i < n) ✓ positiveCompute the quotient q and remainder r of a ÷ b using only subtraction. The archetypal delete a conjunct derivation.
# Specification
# pre Q: a ≥ 0 and b > 0
# post R: a = q*b + r and 0 ≤ r < bStrategy — delete a conjunct. The postcondition is (a = q*b + r) ∧ (0 ≤ r) ∧ (r < b). Drop the hardest conjunct r < b; what remains is the invariant.
Guard, bound, init. The guard is the deleted conjunct negated: B: r ≥ b, so on exit P ∧ ¬B yields the full postcondition. Bound t = r. Initialise q := 0; r := a: then a = 0*b + a and a ≥ 0 from the precondition, so P holds.
# {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
# r-b ≥ 0 since r ≥ b ✓ 0 ≤ r held
# bound: r-b < r (b > 0) ✓ decreased
# t > 0 while r ≥ b > 0 ✓ positiveFind the first index i in b[0..n-1] where b[i] = x, given that x is known to occur. This shows the enlarge the range flavour, and how the precondition does design work.
# Specification
# 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]Strategy — enlarge the range. Let i range over the scanned prefix, asserting that x has not been seen yet and is still present from i onward.
Guard, bound, init. Loop while the current cell is not the target: B: b[i] ≠ x. On exit b[i] = x, and P already carries x not in b[0..i-1], giving R. Bound t = n - i. Initialise i := 0: the prefix b[0..-1] is empty and the precondition supplies x in b[0..n-1], so P holds.
# {x occurs in b[0..n-1]}
i := 0 ;
# invariant P (above)
# bound t: n - i
do b[i] ≠ x →
i := i + 1
od
# {0 ≤ i < n and b[i] = x and x not in b[0..i-1]}# before body: b[i] ≠ x, and P says
# x occurs in b[i..n-1]
# since b[i] ≠ x, x must lie in b[i+1..n-1]
# ⇒ after i:=i+1, x occurs in b[i'..n-1] ✓
# and x not in b[0..i] (b[i]≠x added) ✓
# i never exceeds n-1: x present ⇒ i<n always,
# so b[i] is defined and never runs off ✓
# bound: n-(i+1) < n-i, and > 0 while looping ✓The precondition (“x is present”) is precisely what keeps the invariant’s last conjunct alive and stops the loop from indexing past n-1. Drop it and the derivation tells you exactly what breaks: you would need the compound guard i < n cand b[i] ≠ x to guard the array access.
Find an index k of a maximum element of a non-empty array b[0..n-1]. Another replace a constant by a variable, now with a branching body.
# Specification
# pre Q: n ≥ 1
# post R: 0 ≤ k < n and (∀ j : 0 ≤ j < n : b[k] ≥ b[j])Strategy — replace a constant by a variable. Replace the fixed range bound n by a variable i: k indexes the maximum of the processed prefix b[0..i-1].
Guard, bound, init. Guard B: i ≠ n; on exit i = n makes the quantifier range over the whole array, giving R. Bound t = n - i. Since n ≥ 1, initialise k := 0; i := 1: the prefix b[0..0] has its lone element as maximum, so P holds.
# {n ≥ 1}
k := 0 ; i := 1 ;
# invariant P: 0 ≤ k < i ≤ n and
# (∀ j:0≤j<i: b[k] ≥ b[j])
# bound t: n - i
do i ≠ n →
if b[i] > b[k] → k := i
[] b[i] ≤ b[k] → skip
fi ;
i := i + 1
od
# {0 ≤ k < n and (∀ j:0≤j<n: b[k] ≥ b[j])}# before body: b[k] ≥ b[j] for all j < i
# need: after processing b[i], b[k'] is
# max over j < i+1.
# case b[i] > b[k]: k':=i, so b[k']=b[i]
# ≥ b[k] ≥ b[j] (j<i), and ≥ b[i] ✓
# case b[i] ≤ b[k]: skip, b[k] still ≥ all
# j<i, and b[k] ≥ b[i] ✓
# guards cover all cases (total if) ✓
# bound: n-(i+1) < n-i, > 0 while i≠n ✓Compute z = XY for Y ≥ 0 in a logarithmic number of multiplications. This shows a nontrivial invariant of the shape answer = accumulated × remaining-work.
# Specification
# pre Q: Y ≥ 0 (X, Y are the fixed inputs)
# post R: z = X^YStrategy — generalise with an accumulator (a delete-a-conjunct / combine variant). Introduce evolving variables x, y, z and hold the product of the answer-so-far z with the work-remaining xy constant at XY.
Guard, bound, init. Guard B: y ≠ 0; on exit y = 0 so x0 = 1 and P collapses to z = XY, which is R. Bound t = y. Initialise x := X; y := Y; z := 1: then z * x^y = 1 * X^Y = X^Y and Y ≥ 0, so P holds.
# {Y ≥ 0}
x := X ; y := Y ; z := 1 ;
# invariant P: z * x^y = X^Y and y ≥ 0
# bound t: y
do y ≠ 0 →
if y mod 2 = 0 → x := x * x ; y := y / 2
[] y mod 2 = 1 → z := z * x ; y := y - 1
fi
od
# {z = X^Y}# even branch (y = 2m):
# z * (x*x)^(y/2) = z * (x^2)^m
# = z * x^(2m) = z * x^y = X^Y ✓
# bound y/2 < y (y ≥ 2 here) ✓
# odd branch (y ≥ 1):
# (z*x) * x^(y-1) = z * x^y = X^Y ✓
# bound y-1 < y ✓
# y ≥ 0 kept: y/2 ≥ 0 and y-1 ≥ 0 (y ≥ 1) ✓
# guards cover y even / y odd (total if) ✓
# t = y > 0 while y ≠ 0 ✓Compute the greatest common divisor of two positive integers by repeated subtraction. The invariant preserves a mathematical quantity, not a range.
# Specification
# pre Q: a > 0 and b > 0 (A, B name the initial values)
# post R: result = gcd(A, B)Strategy — combine pre- and postconditions / preserve an invariant quantity. Work with evolving x, y and hold the gcd of the pair fixed at gcd(A, B), keeping both positive.
Guard, bound, init. Guard B: x ≠ y; on exit x = y, and since gcd(x, x) = x, the common value equals gcd(A, B). Bound t = x + y (equivalently max(x, y)). Initialise x := a; y := b, so P holds trivially.
# {a > 0 and b > 0}
x := a ; y := b ;
# invariant P: gcd(x,y) = gcd(A,B) and x>0 and y>0
# bound t: x + y
do x ≠ y →
if x > y → x := x - y
[] y > x → y := y - x
fi
od ;
result := x
# {result = gcd(A, B)}# key identity: gcd(x,y) = gcd(x-y, y) for x > y
# case x > y: x':=x-y
# gcd(x-y, y) = gcd(x, y) = gcd(A,B) ✓
# x-y > 0 since x > y, y unchanged > 0 ✓
# case y > x: symmetric ✓
# guards cover x>y / y>x; x=y excluded
# by the loop guard (total if) ✓
# bound: subtracting a positive from one
# term drops x+y; stays > 0 ✓Given an array of elements coloured red, white, or blue, rearrange it in a single pass so all reds precede all whites, which precede all blues. Dijkstra’s problem; the invariant is best read as four regions.
# Specification
# pre Q: b[0..n-1] holds reds, whites, blues in any order
# post R: b is a permutation of its input, ordered
# red* white* blue*Strategy — enlarge the range / three growing regions. Maintain three boundaries carving b into four regions. Reds occupy [0..lo-1], whites [lo..mid-1], an unknown middle [mid..hi], and blues [hi+1..n-1]. The loop shrinks the unknown region to empty.
Guard, bound, init. Loop while the unknown region is non-empty: B: mid ≤ hi. Bound t = hi - mid + 1 (the size of the unknown region). Initialise lo := 0; mid := 0; hi := n-1, so every element is unknown and the three coloured regions are empty — P holds.
# {b[0..n-1] holds reds/whites/blues}
lo := 0 ; mid := 0 ; hi := n - 1 ;
# regions: red[0..lo-1] white[lo..mid-1]
# unknown[mid..hi] blue[hi+1..n-1]
# bound t: hi - mid + 1 (unknown size)
do mid ≤ hi →
if b[mid] = red →
swap(b[lo], b[mid]) ; lo := lo+1 ; mid := mid+1
[] b[mid] = white →
mid := mid + 1
[] b[mid] = blue →
swap(b[mid], b[hi]) ; hi := hi - 1
fi
od
# {red* white* blue*}# b[mid]=red: swap places a red at lo, a white
# (from [lo..mid-1]) at mid; lo,mid advance
# ⇒ red and white regions still valid ✓
# unknown size (hi-mid+1) drops by 1 ✓
# b[mid]=white: already in place, mid++
# ⇒ white region grows; size drops by 1 ✓
# b[mid]=blue: swap sends it past hi, hi--
# ⇒ blue region grows; the swapped-in
# value stays unknown at mid; size drops 1 ✓
# guards cover red/white/blue (total if) ✓
# exit mid > hi: unknown empty ⇒ sorted ✓Note the asymmetry in the bound: the red and white branches advance mid, while the blue branch retreats hi. Either way hi - mid + 1 strictly decreases, so the single pass terminates in n steps.
Work through the state changes and the exact claim being checked.
| Step | Evidence, decision, and expected result |
|---|---|
| Specify input and output | Input contains only red/white/blue; output is a permutation with colors grouped. Empty input is permitted. |
| Maintain four regions | Red prefix, white region, unknown middle, blue suffix; also preserve the original multiset. |
| Process one unknown element | Red/white advances the middle; blue swaps with the high boundary and decreases high without skipping the swapped-in unknown. |
| Conclude | Unknown size decreases by one each step. At zero, ordering plus permutation proves the required rearrangement. |
No. Include the permutation/multiset relation, or separately prove every mutation is a swap.
Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:
python3 guide_labs.py arithmetic
python3 guide_labs.py testThe complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.
The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.
| Example | Invariant strategy it illustrates |
|---|---|
| 1. Sum of an array | Replace a constant by a variable — generalise the fixed bound n into a growing i. |
| 2. Integer division | Delete a conjunct — drop r < b; the dropped term becomes the guard. |
| 3. Linear search | Enlarge the range — scan a growing prefix; the precondition keeps the index in bounds. |
| 4. Maximum of an array | Replace a constant by a variable — k tracks the max of the prefix b[0..i-1]. |
| 5. Fast exponentiation | Accumulator invariant — answer × remaining-work held constant (z * x^y = X^Y). |
| 6. Euclid’s GCD | Preserve an invariant quantity — gcd(x, y) held fixed via gcd(x,y)=gcd(x-y,y). |
| 7. Dutch National Flag | Enlarge the range / shrinking region — four regions, unknown middle driven to empty. |
P ∧ ¬B. The correctness argument is written before the code, not after it.