DS&A

Is Your Algorithm Correct?

When we write an algorithm to solve a problem, the algorithm is only correct if it does actually solve that problem. That should be obvious! But how do we know whether an algorithm is correct?

This is a genuine concern because algorithms often aren’t correct, and we need to debug them. We need a way to analyse an algorithm to decide if it really does solve the problem or not.

So far, we’ve done this by testing. By actually running the algorithm with particular inputs, we can see whether it gives the expected (correct) output. If it doesn’t, that proves the algorithm is incorrect. On the other hand, testing alone isn’t enough to be sure the algorithm is correct — only that the algorithm gives the correct output for the few inputs we tested.

Example

Consider the following simple algorithm which computes x * x * x * x with two multiplications instead of three:

def fourth_power(x):
    y = x * x
    z = y * y
    return z

With some testing, we can confirm the output is correct in some test cases:

>>> fourth_power(2)
16
>>> fourth_power(-3)
81
>>> fourth_power(0)
0

This is evidence, but not proof, that the algorithm is correct. To prove it, instead of trying some particular inputs, we can imagine running the algorithm without knowing the value of x:

• After the first line, y is equal to x * x.
• After the second line, z is equal to y * y.
• Therefore using both facts, z is equal to (x * x) * (x * x), which is the correct result because the brackets don’t matter.

So, we have proved this algorithm is correct!

Assertions

The key technique we used was to state facts at particular points in the code, and use those to deduce other facts at other points in the code. These statements are called assertions, and we can actually make them in Python:

def fourth_power(x):
    y = x * x
    assert y == x * x

    z = y * y
    assert z == y * y
    assert z == x * x * x * x
    
    return z

Each assert statement makes a claim about the program state at a particular point in its execution; “whenever this line is reached, this condition is true”.

The assertions are not part of the algorithm — think of them like comments explaining why the algorithm is correct. However, unlike comments, the computer will check to make sure assertions are true.

That has a cost in running time — this function now does seven multiplications instead of two — so normally we’d disable assertion-checking once we’ve finished testing the software.

If the algorithm isn’t correct, then an assertion will fail, raising an error. For example, the following function is supposed to calculate x ** 2, but doesn’t:

>>> def incorrect_square(x):
...     y = x + x
...     assert y == x ** 2
...     return y
...
>>> incorrect_square(5)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 3, in incorrect_square
AssertionError

We can see that the assertion failed. To make debugging easier, we could include a message:

>>> def incorrect_square(x):
...     y = x + x
...     assert y == x ** 2, "{} ** 2 isn't {}".format(x, y)
...     return y
... 
>>> incorrect_square(5)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 3, in incorrect_square
AssertionError: 5 ** 2 isn't 10

Preconditions and postconditions

An assertion made before a section of code is a precondition, and an assertion made afterwards is a postcondition.

assert y == x * x
z = y * y
assert z == x * x * x * x

Correctness

For an algorithm to be correct, it must always return the correct output. To prove this, we need to specify the output with an assertion — in this case, the problem was to compute x * x * x * x, so the postcondition z == x * x * x * x is exactly what’s required.

More generally, to prove an algorithm is correct, we must specify the correct output as the algorithm’s postcondition, then prove it really is a postcondition.

The algorithm as a whole may also have a precondition — for example, the binary search algorithm only works if the input list is in order.

Conclusion

The purpose of an assertion is to make a claim about the program state, which should always be true when a particular line of the code is reached. If an assertion fails, it indicates the code before it is incorrect.

Assertions are the basic components of correctness proofs. By dividing an algorithm into sections of code, we can prove for each section that if the precondition is true, then the postcondition will also be true.

However, in this post we only saw how to do this for simple algorithms, where each section of code is executed in sequence. In the next post we’ll see how to extend this reasoning to algorithms with loops.

data = get_user_data(user)
assert data is not None, "User doesn't exist"
save_data_to_file(data)

data = get_user_data(user)
if data is None:
    raise ValueError("User doesn't exist")
save_data_to_file(data)

Footnotes

• Tags: 
• assertions, correctness, algorithms