← Back to System Internals

Two Larger Developments

Two non-trivial algorithms — the Welfare Crook and Saddleback search — derived end to end from their specifications, in the style of Gries’ larger program developments. The invariant is discovered first; the moves are justified by preservation; termination falls out of the bound.

The small examples show the machinery on toy problems where you could have guessed the code anyway. The point of a larger development is to show the same discipline scaling to algorithms you would not want to guess — where a plausible-looking loop is subtly wrong, and only the invariant tells you which move is safe. Both problems below are classic Gries-chapter-20-style developments: the answer is a three-line loop, but every line is forced by a preservation argument you can check.

The method, restated for hard problems

On a hard problem the temptation is to reach for a remembered pattern — “oh, this is the three-pointer trick” — and hope you place the pointers correctly. Gries’ discipline replaces that with a fixed sequence you can follow even when you have never seen the problem:

1. Write the specification as two predicates — a precondition Q and a postcondition R, with quantifiers made explicit over the arrays.
2. Invent an invariant P by weakening R — typically delete a conjunct, or enlarge the region a set of variables ranges over. P must be cheap to establish at the start and, together with a false guard, must imply R.
3. Read off the guard B: the loop runs while P has not yet been narrowed to R.
4. Choose a bound t: a non-negative integer expression the body strictly decreases, which forces termination.
5. Derive the body as the only move that both preserves P and shrinks t. This is the step where the invariant earns its keep — it tells you which candidate move is safe and which quietly loses the answer.

Problem 1: The Welfare Crook

Gries’ famous example (attributed to W. Feijen). Three lists of names are kept in three offices — say the unemployment office, the welfare office, and the payroll of a company. Each list is sorted ascending with no duplicates. Someone is known to be drawing unemployment, collecting welfare, and holding a job at once — so some value occurs in all three lists. Find it. Concretely: given ascending arrays a[0..na-1], b[0..nb-1], c[0..nc-1], find indices i, j, k with a[i] = b[j] = c[k].

Specification

The precondition records what we are told; the postcondition records the three indices we must produce.

# Specification — the Welfare Crook
# pre  Q:  a[0..na-1], b[0..nb-1], c[0..nc-1] each ascending,
#          and  (∃ x, p, q, r ::  a[p] = x ∧ b[q] = x ∧ c[r] = x)
#          i.e. SOME value occurs in all three arrays.
#
# post R:  0 ≤ i < na  ∧  0 ≤ j < nb  ∧  0 ≤ k < nc
#          ∧  a[i] = b[j]  ∧  b[j] = c[k]

Finding the invariant

The postcondition is a conjunction: the indices are in range and they point at a common value. Following delete a conjunct, we drop the equality conjunct a[i] = b[j] = c[k] and keep “in range.” But that alone is far too weak — it would let the loop wander anywhere. The craft of a larger development is picking the right weakening. We instead keep a stronger memory of what we know: a common value still exists at or beyond all three current indices.

Read the last conjunct carefully: it says the “still-searchable” tails of the three arrays — the parts from the current indices onward — still share a common value. The precondition establishes P for free at i = j = k = 0, because then the tails are the whole arrays, which we are told share a value.

The guard. We are done exactly when the three current elements already agree. So we loop while they do not:

The bound. Every move advances one index and none ever retreats, so the total distance left to travel only shrinks:

Why advancing the minimum is the only safe move

This is the crux of the whole development — the step you cannot guess safely without the invariant. Suppose the guard holds, so the three elements are not all equal. Then they are not all the same value, so one of a[i], b[j], c[k] is strictly the smallest (if two tie for smallest they still cannot equal the third, or the guard would be false). Say a[i] is that unique-or-tied minimum. Claim: a[i] cannot be the common value x promised by the invariant.

Argument. The invariant says some x occurs in all three tails, in particular in b[j..nb-1] and c[k..nc-1]. Because b and c are ascending, every element of those tails is ≥ b[j] and ≥ c[k] respectively. So the common value satisfies x ≥ b[j] and x ≥ c[k]. But a[i] is strictly less than at least one of b[j], c[k] (it is the minimum and not all three are equal), hence a[i] < x. Therefore a[i] ≠ x, and since a is ascending, no element of a[i..na-1] equal to a[i] can be x either — the crook’s value must lie strictly to the right of i. It is therefore safe to advance i: doing so discards only a[i], which we just proved is not the common value, so the “common value still exists in all three tails” conjunct survives. The same argument holds by symmetry for whichever array holds the minimum.

The derived program

# {a, b, c ascending; a common value occurs in all three}
i := 0 ;  j := 0 ;  k := 0 ;
# invariant P: a common value occurs in a[i..], b[j..], c[k..]
# bound     t: (na-i) + (nb-j) + (nc-k)
do a[i] ≠ b[j] or b[j] ≠ c[k] →
     # advance whichever index holds a strict minimum:
     if a[i] ≤ b[j] and a[i] ≤ c[k] → i := i + 1
     [] b[j] ≤ a[i] and b[j] ≤ c[k] → j := j + 1
     [] c[k] ≤ a[i] and c[k] ≤ b[j] → k := k + 1
     fi
od
# {a[i] = b[j] = c[k]}  — i, j, k index the common value

# before body: guard holds, so not all equal.
# Some element is a (weak) minimum; the inner IF's
# guards cover every case (≥ is total), so the
# command never aborts — at least one arm is live.
#
# Say a[i] is the chosen minimum and a[i] ≠ x.
# Common value x satisfies x ≥ b[j] and x ≥ c[k],
# and a[i] < x (min, not all equal) ⇒ a[i] ≠ x.
# a ascending ⇒ x lies in a[i+1..na-1].
# So x still occurs in all three tails after i:=i+1
#   ⇒ P preserved.                             ✓
# One index rose by 1 ⇒ t dropped by 1.        ✓

Note the inner if uses ≤ in every guard, so ties are handled and the guards are exhaustive (for any three values at least one is ≤ the other two). Whichever arm fires advances an index whose element is a minimum — exactly the safe move justified above.

Correctness & termination

Discharge the five-part checklist.

Why an index never runs off the end (no array overrun). This is the subtle point that termination and safety both lean on. Suppose the loop is about to advance i because a[i] is the minimum. The invariant guarantees the common value x occurs in a[i..na-1], and we proved a[i] ≠ x, so x occurs strictly within a[i+1..na-1] — which means i+1 ≤ na-1, i.e. i is safely incrementable and stays ≤ na-1. The invariant’s existential conjunct is precisely what forbids stepping past the array. This is the same phenomenon as the linear-search example: the “value is present” precondition is doing design work, here guaranteeing every advance lands on a real element.

Termination. t is a non-negative integer (each index is bounded by its array length) that strictly decreases every iteration, so the loop cannot run forever; it must reach a state where ¬B, i.e. all three elements agree. Combined with obligation 3, that state satisfies R. The algorithm is totally correct, and it does so in at most na + nb + nc iterations — linear in the combined input size.

Problem 2: Saddleback search

A matrix M[0..m-1][0..n-1] is sorted ascending along every row and down every column. A value x is known to be present. Find a cell (r, c) with M[r][c] = x. The name is Gries’: you search from a saddle corner — the top-right — where moving one way only increases values and the other only decreases them, so each comparison eliminates a whole row or a whole column at once.

Specification

# Specification — Saddleback search
# pre  Q:  (∀ p, s ::  s < n-1  ⇒  M[p][s] ≤ M[p][s+1])   (rows ascending)
#          (∀ p, s ::  p < m-1  ⇒  M[p][s] ≤ M[p+1][s])   (cols ascending)
#          (∃ p, s ::  0 ≤ p < m  ∧  0 ≤ s < n  ∧  M[p][s] = x)  (x present)
#
# post R:  0 ≤ r < m  ∧  0 ≤ c < n  ∧  M[r][c] = x

Finding the invariant

Following enlarge the range: instead of tracking a single cell, track a sub-rectangle that still must contain x, and shrink it. Start the cursor at the top-right corner (r, c) = (0, n-1). The invariant asserts that x, which we are told exists, still lies in the rectangle of rows r..m-1 and columns 0..c:

At the start r = 0, c = n-1, the rectangle is the entire matrix, so the precondition establishes P immediately. The cursor (r, c) sits at the top-right corner of the live rectangle: everything above row r and everything right of column c has already been eliminated.

The guard. We stop when the cursor is on the target. We loop while it is not:

The bound. Each move either drops a column (c := c-1) or drops a row (r := r+1); the number of rows-plus-columns still live only shrinks:

Why each move preserves the invariant

At the cursor M[r][c], compare with x. Two cases when it differs:

• M[r][c] > x ⇒ discard column c, i.e. c := c-1. Because columns are ascending downward, every entry below the cursor in column c is ≥ M[r][c] > x. And the cursor is the top of the live part of column c (rows r..m-1). So no cell in column c within the live rectangle equals x. The whole column is therefore safe to discard; x must lie in columns 0..c-1, so the existential conjunct survives with the smaller c.
• M[r][c] < x ⇒ discard row r, i.e. r := r+1. Because rows are ascending rightward, every entry left of the cursor in row r is ≤ M[r][c] < x. And the cursor is the rightmost live cell of row r (columns 0..c). So no cell in row r within the live rectangle equals x. The whole row is safe to discard; x must lie in rows r+1..m-1, so the existential conjunct survives with the larger r.

The derived program

# {rows ascending; cols ascending; x is present in M}
r := 0 ;  c := n - 1 ;
# invariant P: x lies in rows r..m-1, cols 0..c
# bound     t: c + (m - 1 - r)
do M[r][c] ≠ x →
     if M[r][c] > x → c := c - 1   # value too big: drop column c
     [] M[r][c] < x → r := r + 1   # value too small: drop row r
     fi
od
# {0 ≤ r < m and 0 ≤ c < n and M[r][c] = x}

# before body: guard holds, so M[r][c] ≠ x.
# Guards M[r][c]>x and M[r][c]<x are exhaustive
# under M[r][c]≠x ⇒ IF never aborts.
#
# case > x:  col c (rows r..m-1) all ≥ M[r][c] > x
#           ⇒ x not in col c ⇒ x in cols 0..c-1
#           ⇒ P holds after c:=c-1.            ✓
# case < x:  row r (cols 0..c) all ≤ M[r][c] < x
#           ⇒ x not in row r ⇒ x in rows r+1..
#           ⇒ P holds after r:=r+1.            ✓
# either move drops t by exactly 1.            ✓

Correctness & termination

Why the cursor never leaves the matrix (no array overrun). We must know c := c-1 never underflows below 0 and r := r+1 never overflows past m-1. Obligation 4 supplies exactly this: whenever the guard still holds, t > 0, so the rectangle has more than one cell, so at least one of the moves has room. More precisely, in the > x case the existential conjunct guarantees x lies in columns 0..c but not in column c, so it lies in 0..c-1, forcing c ≥ 1 — the decrement is safe. Symmetrically the < x case forces r ≤ m-2, so the increment is safe. As with the crook, the “x is present” precondition, carried in the invariant, is what guarantees the cursor stays in bounds.

Termination. t = c + (m-1-r) starts at (n-1) + (m-1), is bounded below by 0, and strictly decreases each step, so the loop runs at most m + n - 2 times before reaching ¬B. Combined with obligation 3, exit implies R. Saddleback search is totally correct and runs in O(m + n) — each step retires a whole row or column, which is exactly why it beats a naive per-cell scan.

Summary