Writing robust code is always a good idea, but is particularly important for mission critical contexts, such as where safety is an issue. There are several historical examples of where faulty code led to disaster and loss of life.

Did you know that up to 90% of software engineers fail to correctly implement the Binary Search Algorithm when tested?

One way we can help to ensure the correctness of code is to use something called a loop invariant for iteration. A loop invariant is something that is true:

• before the loop starts
• before each iteration of the loop
• after the loop terminates

Using a loop invariant is a great way to go about actually proving the correctness of an algorithm, in a rigorous mathematical sense, rather than just crossing your fingers and hoping for the best. Of course test driven development can help to verify any number of specific cases, but invariants can be used to prove program correctness for all cases.

Loop invariants can be something of an involved topic, but here I just want to introduce the idea and give a couple of examples to sow the seed. You may well find that even a cursory acquaintance with them can help you to reason more effectively about your code.

LOOP INVARIANTS IN A WHILE LOOP

Let’s say we want to ensure the correctness of a function that sums the numbers in a list. I know such a function already exists in Python, but we are developing our reasoning here, so will implement it ourselves.

def my_sum_while(A):
    """
    Loop Invariant: At the start of iteration i of the loop, the variable
    `total` should contain the sum of the numbers from the subarray A[0:i].
    """
    i = 0
    total = 0
    assert total == sum(A[0:i])
    while i < len(A):
        assert total == sum(A[0:i])
        total += A[i]
        i += 1
    assert total == sum(A[0:i]) and i >= len(A)
    return total

xs = [1, 2, 3, 4, 5]
assert my_sum_while(xs) == 15

The variable name xs in the above code mean “multiple x values.”

Here, the loop invariant is: “At the start of iteration i of the loop, the variable total should contain the sum of the numbers from the subarray A[0:i].”

We are checking this is true in the three required places by use of Python assert statements. These are very simple and very handy. We make a claim (an assertion) at a given point in our program, and if it turns out our claim is wrong, an AssertionError is thrown and the code stops running. If instead the code gets to the end with no assertion errors, we know that our code is correct at least in terms of the checks we have made with our assertion statements.

LOOP INVARIANTS IN A FOR LOOP

Things get a little confusing with for loops, because there is no manual initiation of the counter variable, and the loop exits one check of the loop condition (i.e. the counter value) earlier than an equivalent while loop. This can mean that a given invariant in a for loop looks different from its equivalent in a while loop. In order to enhance the clarity of the following example (in my opinion), I have initialised i to 0 before entering the loop, and performed one extra increment before the final assertion. This enables us to keep the invariant exactly as given, without the need to adjust for “off by one” errors.

def my_sum_for(A):
    """
    Loop Invariant: At the start of iteration i of the loop, the variable
    `total` should contain the sum of the numbers from the subarray A[0:i].
    """
    total = 0
    i = 0
    assert total == sum(A[0:i])
    for i in range(len(A)):
        assert total == sum(A[0:i])
        total += A[i]
    i += 1
    assert total == sum(A[0:i]) and i >= len(A)
    return total

xs = [1, 2, 3, 4, 5]
assert my_sum_for(xs) == 15

LOOP INVARIANTS CHALLENGE

Here’s a challenge from Maths that can be solved nicely using invariants.

Suppose the positive integer n is odd. First Al writes the numbers 1, 2,..., 2n on the blackboard. Then he picks any two numbers a, b, erases them, and writes, instead, |a − b| (that is, abs(a - b)). Prove that an odd number will remain at the end.

If you like, try and find an invariant you can use to prove this, before clicking on “show solution” and looking at the code below.

Hint: What is the formula for the Triangle Numbers?

• This may not be obvious. Get out a pen and paper or mini whiteboard and play around with some examples until you are convinced.

import random


def invariant_example(n):
    xs = [x for x in range(1, 2*n+1)]
    print(xs)
    assert sum(xs) % 2 == 1
    while len(xs) >= 2:
        assert sum(xs) % 2 == 1
        a, b = random.sample(xs, 2)
        print(f"a: {a}, b: {b}, xs: {xs}")
        xs.remove(a)
        xs.remove(b)
        xs.append(abs(a - b))
    assert sum(xs) % 2 == 1 and len(xs) < 2
    print(f"Final state of xs: {xs}")
    return


invariant_example(5)

Try typing in and running the code. Then spend some time if you need to really thinking about how it works. Add comments to your code if it helps to understand and follow what is happening at various points.

This article has discussed the use of loop invariants in Python to help to develop the skill of writing robust code. I hope you have found it interesting and useful.

Happy computing!

Sharing is caring!