← Back to System Internals

Efficiency — Strengthening Invariants

Gries’ discipline does not stop at a correct program. Once a loop is proven, you can make it faster by the same calculus that made it correct — not by abandoning the invariant, but by strengthening it so an expensive quantity is carried along and maintained incrementally instead of recomputed from scratch.

There is a folk belief that making a program fast means bending or breaking its clean structure — that correctness and speed pull in opposite directions. Gries shows the reverse. The most reliable optimisation of a loop is a program transformation that adds a new variable and a new conjunct to the invariant, so that a term the loop was recomputing on every pass is instead updated in a step or two. The invariant gets stronger, the program gets faster, and the correctness argument gets richer rather than weaker. This is the same move behind “strength reduction” and “loop-invariant code motion” in compilers — here derived by hand, with proof.

Correctness first, then efficiency

The order of operations is not negotiable. First derive a correct loop from its specification, invariant, and bound — exactly the discipline of the earlier chapters. Then, and only then, look at it as an object to be improved. Efficiency is a second pass over a program you already trust.

The crucial claim is about how you improve it. You do not weaken the invariant to give the compiler or yourself more room; a weaker invariant proves less, and a loop that proves less is a loop you no longer trust. Instead you strengthen the invariant by adding a conjunct that records some quantity, and then you have a new obligation — to keep that conjunct true — whose cheapest discharge is an incremental update. The speed comes precisely from the extra thing you now guarantee.

Read it as a transformation with a contract: the transformed loop must compute the same result as the original (same postcondition), so every step is a semantics-preserving rewrite justified by the invariant, not a hopeful edit. Because it is provably equivalent, you get the speed without reopening the question of correctness.

Taking an expression out of a loop

Here is the core move in its plainest form. Suppose the loop body evaluates some expression E on every iteration, where E depends on the loop’s variables, and computing E from scratch is expensive — a sum over a prefix, a power, a running product, a scan. If E changes only a little from one iteration to the next, you are paying full price for a small delta.

The fix: introduce a fresh variable e, and add the conjunct e = E to the invariant. Now e always holds the current value of E. Establish it once in the initialisation, maintain it with a cheap update in the body wherever the loop changes the variables E depends on, and replace every use of E by e.

The obligation the new conjunct creates is exactly what tells you the update. Whatever the body does to the underlying variables, you must restore e = E before the iteration ends. Solving that little equation — “what must I add to e so that it again equals the new E?” — is the whole trick, and it is pure algebra.

Worked example: running sum

Compute s = Σ b[0..n-1], the sum of the first n elements of an array. Derive it first, then observe the waste, then transform.

# Specification
# pre  Q:  n ≥ 0
# post R:  s = (sum j : 0 ≤ j < n : b[j])

Replace the constant n by a variable i to get the loop invariant — the answer computed so far, over the prefix b[0..i-1]:

The naive way to write the body is to take the invariant literally and, after bumping i, recompute the whole prefix sum. That re-adds b[0], b[1], … from the start on every pass — the loop is O(n) iterations each doing O(i) work, so O(n²) overall. But the strengthened form already holds the sum in s; the only change from one iteration to the next is one new term b[i]. So s := s + b[i] restores the invariant in O(1).

i := 0 ;  s := 0 ;
do i ≠ n →
     i := i + 1 ;
     # re-derive s from scratch over b[0..i-1]
     s := 0 ;
     k := 0 ;
     do k ≠ i →
          s := s + b[k] ;  k := k + 1
     od
od
# E = (sum j:0≤j<i:b[j]) recomputed every pass
# total work: O(n²)

i := 0 ;  s := 0 ;
# invariant P: 0 ≤ i ≤ n and
#             s = (sum j:0≤j<i:b[j])
# bound     t: n - i
do i ≠ n →
     s := s + b[i] ;   # restore s = sum over 0..i
     i := i + 1        # now s = sum over 0..(new i)-1
od
# {s = (sum j:0≤j<n:b[j])}
# total work: O(n)

The strengthened conjunct s = Σ b[0..i-1] was already in the invariant — that is the point. The naive body discards it and rebuilds; the good body uses it, adding only the delta b[i]. Note the update order: add b[i] while i still points at the new element, then advance i, so that s = Σ b[0..i-1] holds again at the bottom of the loop.

Worked example: strength reduction on squares

Print (or store) i*i for i = 0, 1, …, n using no multiplication at all — only addition. On machines where a multiply is far dearer than an add, this is a real win, and it is the textbook case of strength reduction: replacing an expensive operation with a cheaper one maintained incrementally.

# Goal: at each step have sq = i*i, for i = 0..n, using only +
# Expensive expression E = i*i

Add the conjunct sq = i*i to the invariant. The body increments i, so we must find the cheap update that restores sq = i*i for the new i. The algebra:

(i+1)² = i² + 2i + 1
# so when i becomes i+1, sq must grow by (2i + 1)

But 2i + 1 still contains a multiplication. Apply the technique a second time: introduce another variable d with the conjunct d = 2i + 1, the amount by which sq must increase. When i becomes i+1, the increment itself changes: 2(i+1) + 1 = (2i + 1) + 2, so d grows by the constant 2. Now nothing multiplies.

i := 0 ;
do i ≠ n + 1 →
     use(i * i) ;      # E = i*i recomputed
     i := i + 1
od
# one multiplication per iteration

i := 0 ;  sq := 0 ;  d := 1 ;
# invariant P: sq = i*i and d = 2*i + 1
# bound     t: (n + 1) - i
do i ≠ n + 1 →
     use(sq) ;         # sq = i*i, no multiply
     sq := sq + d ;    # (i+1)² = i² + (2i+1)
     d  := d + 2 ;     # 2(i+1)+1 = (2i+1) + 2
     i  := i + 1
od
# init check: i=0 ⇒ sq=0=0², d=1=2·0+1 ✓

Each derivation step was forced. The update sq := sq + d came from expanding (i+1)²; the update d := d + 2 came from expanding 2(i+1)+1; the initial values sq = 0, d = 1 came from substituting i = 0 into the two new conjuncts. Nothing was guessed. This double application is characteristic: reducing one expression often exposes another, and you strengthen again until only constants remain.

Worked example: maintaining a power

Suppose a loop needs x^i at each step for i = 0, 1, …, n. Recomputing pow(x, i) from scratch costs O(i) multiplications per pass (or O(log i) with fast exponentiation) — wasteful when consecutive powers differ by a single factor of x.

Add the conjunct p = x^i to the invariant. Since x^(i+1) = x^i · x, the update that restores it when i advances is a single multiplication, p := p*x. The base case x^0 = 1 gives the initialisation.

i := 0 ;
do i ≠ n + 1 →
     use(pow(x, i)) ;   # E = x^i from scratch
     i := i + 1
od
# O(i) (or O(log i)) mults every pass

i := 0 ;  p := 1 ;      # x^0 = 1
# invariant P: p = x^i
# bound     t: (n + 1) - i
do i ≠ n + 1 →
     use(p) ;           # p = x^i
     p := p * x ;       # x^(i+1) = x^i · x
     i := i + 1
od

This is the same idea that underlies fast exponentiation, where an invariant of the form result * base^exp = x^n is maintained while exp is halved — each step preserves a product-shaped invariant with a cheap update. See the exponentiation derivation in the worked examples: the discipline is identical, only the invariant’s shape differs. Whenever a quantity you need next iteration is a simple function of the one you have now, an invariant conjunct turns recomputation into a single step.

The general recipe

Every example above is the same five moves. Here they are as a checklist you can run on any proven loop that recomputes something.

1. Spot a recomputed expression E. Look in the body for a term, written in the loop’s variables, that is evaluated every pass and is expensive relative to the rest of the iteration — a sum, a product, a power, a scan, a repeated index computation.
2. Add the conjunct e = E to the invariant. Introduce a fresh variable e whose sole job is to always equal E. This strengthens the invariant — you now promise more.
3. Fix the initialisation to establish it. Set e to the value of E in the loop’s starting state (substitute the initial values of the variables into E), so e = E holds before the first iteration.
4. Derive the incremental update. Given how the body changes the variables E depends on, solve for the cheap adjustment to e that re-establishes e = E at the bottom of the loop. This algebra is the heart of the transformation; if the adjustment still contains an expensive term, apply the recipe again to it (as with the squares example).
5. Replace uses of E by e. Every place the body read E, read e instead. The expensive computation is now gone from the body, replaced by a value that was maintained cheaply.

Note that steps 2 through 5 mirror exactly the four loop obligations from the correctness checklist — establish the invariant, preserve it, and use it — applied to the new conjunct. That is why the transformation cannot break correctness: it discharges its own proof obligation by construction.

Trade-offs

The transformation is nearly free in correctness terms but not free in every other sense. Weigh it honestly.

When not to bother. If E is already cheap (a couple of additions), the extra variable and update line buy nothing and cost clarity. If the loop is cold — run rarely, or over tiny inputs — the constant-factor win is invisible and the readability tax is real. And if the incremental update turns out to be as expensive as recomputing E, there is no delta to exploit; the technique only pays when E changes little between iterations.

Summary