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:
package Math with SPARK_Mode is subtype Value is Integer range 0 .. 10_000; type Index is range 1 .. 100; type Values is array (Index) of Value; function Sorted (V : Values) return Boolean is (for all J in Index'First .. Index'Last - 1 => V(J) <= V(J+1)); subtype Sorted_Values is Values with Dynamic_Predicate => Sorted (Sorted_Values); procedure Apply_Ratio (V : in out Sorted_Values; Num, Denom : Value) with Pre => Denom /= 0 and then Num <= Denom, Post => (for all J in Index => V(J) = V'Old(J) * Num / Denom); end Math;
The implementation goes over the array, applying the ratio to each element in turn:
package body Math with SPARK_Mode is procedure Apply_Ratio (V : in out Sorted_Values; Num, Denom : Value) is begin for J in Index loop V(J) := V(J) * Num / Denom; end loop; end Apply_Ratio; end Math;
In order to prove the postcondition of Apply_Ratio, we must add a suitable loop invariant that states that:
- the ratio has been applied to all elements up to the current element
- 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:
pragma Loop_Invariant (for all K in Index'First .. J => V(K) = V'Loop_Entry(K) * Num / Denom); pragma Loop_Invariant (for all K in J + 1 .. Index'Last => V(K) = V'Loop_Entry(K));
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:
math.adb:7:10: medium: predicate check might fail math.adb:7:29: medium: range check might fail
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:
procedure Lemma_Mult_Scale (Val : Int; Scale_Num : Nat; Scale_Denom : Pos; Res : Int) with Global => null, Pre => Scale_Num <= Scale_Denom and then Res = (Val * Scale_Num) / Scale_Denom, Post => abs (Res) <= abs (Val) and then (if Val >= 0 then Res >= 0 else Res <= 0);
Let's call this lemma in our code as follows:
for J in Index loop Lemma_Mult_Scale (Val => V(J), Scale_Num => Num, Scale_Denom => Denom, Res => V(J) * Num / Denom); V(J) := V(J) * Num / Denom; ...
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:
procedure Lemma_Mult_Is_Monotonic (Val1 : Int; Val2 : Int; Factor : Nat) with Global => null, Pre => Val1 <= Val2, Post => Val1 * Factor <= Val2 * Factor; procedure Lemma_Div_Is_Monotonic (Val1 : Int; Val2 : Int; Denom : Pos) with Global => null, Pre => Val1 <= Val2, Post => Val1 / Denom <= Val2 / Denom;
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:
Prev_Value : Value := 0 with Ghost;
which is updated before the assignment to V(J):
Prev_Value := V(J);
and whose value is passed on for proof to the next iteration of the loop through a loop invariant:
pragma Loop_Invariant (Prev_Value = V'Loop_Entry(J));
That's it! We can now call the lemmas in our code as follows:
for J in Index loop Lemma_Mult_Is_Monotonic (Val1 => Prev_Value, Val2 => V(J), Factor => Num); Lemma_Div_Is_Monotonic (Val1 => Prev_Value * Num, Val2 => V(J) * Num, Denom => Denom); pragma Assert (if J > Index'First then V(J - 1) <= V(J) * Num / Denom); Prev_Value := V(J); V(J) := V(J) * Num / Denom; ...
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:
with SPARK.Integer_Arithmetic_Lemmas; use SPARK.Integer_Arithmetic_Lemmas; package body Math with SPARK_Mode is procedure Apply_Ratio (V : in out Sorted_Values; Num, Denom : Value) is Prev_Value : Value := 0 with Ghost; begin for J in Index loop Lemma_Mult_Scale (Val => V(J), Scale_Num => Num, Scale_Denom => Denom, Res => V(J) * Num / Denom); Lemma_Mult_Is_Monotonic (Val1 => Prev_Value, Val2 => V(J), Factor => Num); Lemma_Div_Is_Monotonic (Val1 => Prev_Value * Num, Val2 => V(J) * Num, Denom => Denom); pragma Assert (if J > Index'First then V(J - 1) <= V(J) * Num / Denom); Prev_Value := V(J); V(J) := V(J) * Num / Denom; pragma Loop_Invariant (Sorted (V)); pragma Loop_Invariant (Prev_Value = V'Loop_Entry(J)); pragma Loop_Invariant (for all K in Index'First .. J => V(K) = V'Loop_Entry(K) * Num / Denom); pragma Loop_Invariant (for all K in J + 1 .. Index'Last => V(K) = V'Loop_Entry(K)); end loop; end Apply_Ratio; end Math;
[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.