## Invariants

May 142018An assertion is a claim about the state of a running program — it says that some logical condition should be true whenever a particular line of code is reached. In the previous post, we only considered assertions in code where each line is executed once, in sequence.

Of course, real algorithms are more complicated, because loops and recursion cause some code to be executed multiple times, not in a simple sequence. In this post we’ll explore invariants, which are needed to prove correctness of non-trivial algorithms.

#### Analogy

Invariants are a very abstract idea, and can be difficult to understand. We’ll start with an analogy unrelated to algorithms: bishops in the game of chess. Don’t worry if you don’t play chess — all you need to know is that bishops move diagonally.

However many moves you make, this bishop will always be on a white square. This is because:

- It starts on a white square, and
- Any move from a white square lands on a white square.

The assertion that “the bishop is on a white square” is called an *invariant*.
It remains true even though the bishop’s position can change.

An invariant is an assertion — a statement of fact.
For our purposes, the colour of the bishop’s square is **not** an invariant, because although it does stay the same, the square colour is white or black, not true or false.

#### Induction

We said the bishop starts on a white square, and any move from a white square lands on another white square — therefore it will still be on a white square *however many moves you make*.

This last part of the argument is subtle.
We said the invariant is preserved after *one* move, therefore it’s preserved after *any number of* moves.
This kind of argument is called induction.

This is less obvious than it might seem:

- I am in the library.
- If I walk one step, I will still be in the library.
- Therefore, I am stuck in the library forever.

This is clearly nonsense, but it seems like the same kind of argument.

The problem is the second part.
It may be true that from my current location, the *first* step is not enough to exit the library.
However, it’s certainly possible that I could later go from inside the library to outside by walking one step.

On the other hand, the bishop can never move from a white square to a black square, not on the first move or any later move; so it really *is* stuck on white squares.

#### Example

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.

#### Tracing

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)`

.

x | n | r | i | r == x ** i |
---|---|---|---|---|

3 | 4 | 1 | 0 | True |

3 | 4 | 3 | 1 | True |

3 | 4 | 9 | 2 | True |

3 | 4 | 27 | 3 | True |

3 | 4 | 81 | 4 | True |

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.

#### Loop invariants

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.

#### More invariants

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:

n | i |
---|---|

4 | 0 |

4 | 1 |

4 | 2 |

4 | 3 |

4 | 4 |

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.

#### Discovering preconditions

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`

.

#### Using the loop condition

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`

.

This may seem like a lot of effort to prove something obvious; on the other hand, although it’s a simple example, it demonstrates some important principles and techniques.

#### Conclusion

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.

We also fixed a bug by discovering a precondition for the algorithm to be correct; `n`

must not be negative.
This isn’t unusual; many bugs can be discovered by testing, but if we hadn’t tried proving the algorithm correct, we might never have thought about negative inputs.

#### Footnotes

- In Python,
`print(locals())`

is a simple way to print the entire current state of a function. - There is a special case when
`x`

is zero; 0^{0}is usually undefined. However, in Python`0 ** 0`

is 1, and this doesn’t cause any problems here. - A similar argument can be made for if/else statements:
`if i < n: assert i < n # ... else: assert i >= n # ...`

- This argument requires that there are no
`break`

statements inside the loop.

## There are no published comments.