← Back to System Internals

Worked Examples — From Specification to Correct Program

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.

The theory is only worth as much as the programs it produces. This page collects fully worked derivations: for each problem we state the specification as a pair of predicates, name the invariant-finding strategy that applies, exhibit the invariant P, guard B, and bound function t, present the derived guarded-command program, and close with the algebra showing the loop body preserves P and strictly decreases t. Every line of every program below is forced by the specification — nothing is guessed and patched.

1. Sum of an array

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)  ✓ positive

2. Integer division by subtraction

Compute 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 < b

Strategy — 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     ✓ positive

3. Linear search (x is present)

Find 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.

4. Maximum of an array

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      ✓

5. Exponentiation (fast / binary power)

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^Y

Strategy — 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                          ✓

6. Euclid’s GCD

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            ✓

7. Dutch National Flag

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.

Summary