← CatZep/Engineering Guides/The Science of Programming

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.

Concepts explained in this guide

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.

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.

Worked example: maintain a running prefix sum

Work through the state changes and the exact claim being checked.

Run and change the example

Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:

python3 guide_labs.py optimization
python3 guide_labs.py test

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

Summary