DS&A

Let’s see an example of an invariant in an algorithm. Consider the following simple function which calculates x ** n by multiplication:

def power(x, n):
    r = 1
    i = 0
    
    while i < n:
        r *= x
        i += 1
    
    return r

The algorithm uses a loop to multiply r by x the right number of times. The variable i counts how many multiplications have been made so far; at each step r should equal x ** i.

So, even though i and r change in value, the assertion r == x ** i is an invariant of this loop.

One way to see how an algorithm works is to trace it — that is, work through the execution step-by-step, and write down the values of each variable at each step. We can do this with pen and paper, or by adding print statements to the code.(1)

For example, the table below shows a trace of all four variables, at each step of computing power(3, 4).

Before and after each iteration of the loop, the invariant r == x ** i remains true, even as the values of r and i change.

Tracing is also a good way to discover invariants, if you don’t already know what they should be. You can identify this relationship between the variables by looking at the trace, just as you might notice by looking at the chess board that the bishop is always on a white square.

We’ve identified that r == x ** i is a loop invariant. This means:

• It’s true before the loop begins.
• If it’s true before an iteration of the loop, then it will still be true afterwards.
• Therefore it’s true on every iteration, and will still be true when the loop stops.

Let’s annotate the loop with some assertions:

def power(x, n):
    # the invariant must be true before the loop
    r = 1
    i = 0
    assert r == x ** i
    
    while i < n:
        # if the invariant is true here,
        assert r == x ** i
        
        r *= x
        i += 1
        
        # then it's still true here
        assert r == x ** i
    
    return r

Before the loop, x ** i is just x ** 0. This is 1, and r is also 1, so the invariant is true to begin with.(2)

We also need to show that the loop preserves the invariant. The loop multiplies r by x, and increases i by 1. So, the new value of r is (x ** i) * x, and the new value of x ** i is x ** (i + 1). These are equal, so the invariant is preserved.

Therefore the invariant will remain true, however many times the loop iterates.

What else can we prove about this loop?

The loop continues while i < n, and i increases by 1 on each iteration. In some sense, it is obvious that the loop stops when i == n. But how do we actually prove this? It turns out we need another loop invariant.

Certainly, i == n isn’t an invariant; it’s not even true before the loop. On the other hand, by looking at the trace you may notice something:

Don’t think too hard; the simple relationship between these variables is i <= n.

while i < n:
    # if the invariant is true here,
    assert i <= n
    
    r *= x
    i += 1
    
    # then it's still true here
    assert i <= n

Let’s check whether i <= n really is an invariant.

• Before the loop, i = 0, so the invariant holds if 0 <= n.
• For the loop to make an iteration, the condition i < n must be true. The loop increases i by 1, but if i < n then i + 1 <= n. So the invariant is preserved.

There are two points arising from this proof; both are worth addressing.

The invariant must hold before the loop begins. This means we need 0 <= n to be true — but this is not guaranteed!

By trying to prove the invariant, we actually discovered a precondition for our algorithm — n must not be negative. To avoid incorrect behaviour, we should reject the input if it’s invalid:

def power(x, n):
    if n < 0:
        raise ValueError('n must not be negative')
    
    assert n >= 0
    # ...

By raising an error if n is negative, we can safely assert n >= 0. Now the invariant i <= n is guaranteed to hold before the loop, because i = 0.

To prove that the loop preserves the invariant i <= n, we had to show that if it was true at the start of an iteration, then it would still be true afterwards.

This worked because at the start of an iteration, we can assert i < n. This assertion can never fail, because otherwise the loop would not have made another iteration.(3)

while i < n:
    assert i < n
    # ...

assert i >= n

We can also assert i >= n when the loop stops. This assertion can’t fail; if it were false, the loop wouldn’t have stopped.(4)

This is enough to prove that i == n after the loop:

• The loop invariant i <= n must be true after the loop.
• The assertion i >= n is also true after the loop.
• The only way this can happen is if i == n.

Using invariants, we proved that r == x ** i and i == n are postconditions of this loop. Together, these imply r == x ** n, meaning the algorithm returns the correct result.