Proving asymptotic time complexity bounds with SPARK

The SPARK user’s guide has a nice chapter about how to write loop invariants. It walks you through an example of a linear search function together with contracts and loop invariants that make it possible for GNATprove to verify the functional correctness of the function. Later, it presents a binary search function, again with annotations ensuring functional correctness.

What the SPARK user’s guide doesn’t touch on, however, is the purpose of the binary search function. It’s harder to use than the linear search function because the input array needs to be sorted. Its body is also more complex. So, what is the point of the binary search function? That is, other than as a loop invariant drill.

The answer is, of course, that binary search can be much faster than linear search. This is characterized by the time complexity of these algorithms. Binary search is said to run in logarithmic time, while linear search is fittingly said to run in linear time.

The question is: can SPARK be used to prove something about the time complexities of Linear_Search and Binary_Search? Let’s be honest: SPARK was not designed for serious time complexity proof work. But if we’re willing to indulge in a bit of recreation, we’ll see that we can twist it into verifying some interesting properties.

General Approach

The time complexity bounds that we’ll look at all follow the same pattern. First, we’ll add a pair of local ghost variables to the function of interest:

N is going to represent the size of the input. In our examples, it will always be the length of the input array.

We will use Counter to keep track of how long the function has been running. For this, we will “ignore constant factors” as is customary with time complexity. In practice, this will mean doing our best to follow this simple rule:

At each loop iteration, we must increment Counter. ¹

SPARK will not be able to help us verify that we do this part correctly so we will need to be very careful.

Using N and Counter, we will annotate every return point in the function of interest with an assertion that makes a meaningful claim about time complexity.

We will then ask GNATprove to verify these assertions. It’s very likely that it won’t be able to prove them right away; we’ll need to write the right loop invariants to make the proof pass.

Linear Search

Let’s see how this works out on the linear search example. Here’s the code, with all the additions we discussed before except the extra loop invariant. These additions are highlighted.

As it stands, GNATprove is not able to prove these assertions. For this, we need an additional loop invariant:

There is a bit of noise because of conversions between the bounded integer types we use for the concrete code and the arbitrary-precision types we use for the ghost variables. And we have to keep in mind that an array in Ada has a lower bound and an upper bound and not just a length as is common in other languages. But the loop invariant is otherwise straightforward. It uses the loop index Pos to connect N with Counter inside the loop, and GNATprove is able to take it from there.

Binary Search

The time complexity of binary search is logarithmic. This means that Counter is not greater than the logarithm of N. To make things easier, we’re going to go with the equivalent property that 2 to the power of Counter is not greater than N.

About the details of how we’re going to achieve that, I’ve got good news and bad news. The good news is that Ada has a concise operator for exponentiation, **, and that the Big_Integers package has a definition of it. The bad news is that since that definition takes a bounded integer for the exponent, we’re not going to be able to make use of it and we’ll need to roll our own function:

Let’s apply our method to the binary search function:

Coming up with the loop invariant takes a bit of work (perhaps with pen and paper). For our final assertions, we had to settle with Two_Power (Counter) <= 2 * N + 1, instead of the simpler Two_Power (Counter) <= N. This is fine; the two are equivalent under the usual simplifying assumptions of time complexity measurement (i.e., Big-O notation).

This proves cleanly and hence confirms our complexity proof that binary search has logarithmic complexity.

Bonus: more about the Counter rule

As we said earlier, we need to be careful that we don’t break the rule about incrementing Counter in loop bodies. SPARK cannot help us with that. To illustrate this, let’s look at the selection sort example in the SPARK user’s guide, annotated in the style we’ve been following:

This claims that selection sort runs in linear time. This is notoriously wrong: the time complexity of selection sort is quadratic. Yet GNATprove is able to prove the assertions here. Can you tell what the catch is?

The problem is the call to Index_Of_Minimum which does not run in constant time. We need to incorporate Index_Of_Minimum in our analysis to get things right.

Footnotes

[1] If we had any sort of recursion going on, we would also need to increment Counter every time we enter a function body. Since there’s no recursion in the examples we’re looking at, we set aside that part of the rule.