A well-know result of computing theory is that the theory of arithmetic is undecidable: one cannot design an algorithm which takes any arithmetic formula (with quantifiers and the usual arithmetic operators) and returns "true" when it is an "always true" formula. This is already the fact with addition, subtraction and multiplication as only arithmetic operators (called Peano arithmetic). Only when one limits operators to addition and subtraction (called Presburger arithmetic) do we have decision procedures, that is, algorithms to decide if a formula is always true or not.

This has practical consequences in automatic proof of programs which manipulate numbers. The provers that we use in SPARK have a good support for addition and subtraction, but much weaker support for multiplication and division (except for multiplication by an integer constant which is treated as repeated additions). This means that as soon as the program has multiplications and divisions, it is likely that some checks won't be proved automatically. Until recently, the only way forward was either to complete the proof using an interactive prover (like Coq or Isabelle/HOL) or to justify manually the message about an unproved check. There is now a better way to prove automatically such checks, using the recent SPARK lemma library.

Let's see how this works on an example of code, which applies the same ratio to all numbers in a sorted array:

The implementation goes over the array, applying the ratio to each element in turn:

In order to prove the postcondition of Apply_Ratio, we must add a suitable loop invariant that states that:

1. the ratio has been applied to all elements up to the current element
2. all other elements are still equal to their value when entering the loop

Note that this kind of loop is quite common, and the most precise loop invariant (as given above) for these loops is described in the SPARK User's Guide:

With this loop invariant, the postcondition of procedure Apply_Ratio is proved, but two checks are not proved on the assignment to V(J) inside the loop:

Let's start with the unproved range check on V(J) * Num / Denom. We know that this value is between 0 and V(J), because Num / Denom is a ratio, as expressed in the precondition of Apply_Ratio: Num <= Denom. But because this expression involves multiplication and division between variables, current automatic provers have no clue! The solution here is to call a lemma that provides this information in its postcondition. Fortunately, these is such a lemma in the SPARK lemma library:

Let's call this lemma in our code as follows:

Now the range check is proved by GNATprove. So let's turn to the predicate check. The issue is that variable V is of type Sorted_Values which is subject to predicate Sorted. Hence, V should still be sorted after the assignment to V(J). This holds because the array was originally sorted, so applying the same ratio to each element in increasing order (i.e. from left to right) maintains the property that the array is sorted. Mathematically, this relies on the properties of multiplication and division, which are monotonic on natural numbers: given two non-negative values A and B such that A is less or equal to B, multiplying or dividing them by a positive value C results in two values A' and B' such that A' is less or equal to B'. Again, current automatic provers have a hard time figuring this out, so we're going to call lemmas to provide this information. Here they are from the SPARK lemma library:

Now, we need to apply the lemmas to some values. Here, we'd like to apply them to the initial values of V(J-1) and V(J), which need to be maintained in the same order while they are multiplied by Num and divided by Denom. The initial value of V(J) is available before assigning to V(J), but not the initial value of V(J-1) which has been updated already. So we'll use ghost code to make it available at the J'th iteration of the loop, by declaring a local ghost variable in procedure Apply_Ratio:

which is updated before the assignment to V(J):

and whose value is passed on for proof to the next iteration of the loop through a loop invariant:

That's it! We can now call the lemmas in our code as follows:

Note the intermediate assertion which expresses the desired property proved by the use of lemmas. Now, GNATprove proves the intermediate assertion by using the lemmas, and it proves the predicate check by using the intermediate assertion. Here is the final code of the procedure Apply_Ratio, which is fully proved by GNATprove:

[The loop invariant stating that Sorted(V) is currently needed due to how type predicates are handled around loops, but this will soon be inferred automatically by GNATprove.]

The SPARK lemma library thus fills an interesting point in the matrix of techniques between fully automated proof and interactive proof, which can be depicted on this graph:

On the Y axis, the complexity of the property to prove increases. On the X axis, the complexity for the user to apply the technique increases. So we start with the default settings (no user effort), which are good to prove properties with a (possibly complex) boolean structure and linear integer arithmetic, then continue with higher proof levels (switch --level of GNATprove with values 1, 2, 3 or 4) to prove more complex properties with quantifiers and modular arithmetic, then continue with the SPARK lemma library for nonlinear arithmetic, then with intermediate assertions and ghost code (which we used also here), then manual proof using an interactive theorem prover.

For more details about the SPARK lemma library, see the SPARK User's Guide.