7.9.3. Manual Proof Examples
The examples in this section contain properties that are difficult to prove automatically and thus require more user interaction to prove completely. The degre of interaction required depends on the difficuly of the proof:
simple addition of calls to ghost lemmas for arithmetic properties involving multiplication, division and modulo operations, as decribed in Manual Proof Using SPARK Lemma Library
more involved addition of ghost code for universally or existentially quantified properties on data structures and containers, as described in Manual Proof Using Ghost Code
interaction at the level of Verification Condition formulas in the syntax of an interactive prover for arbitrary complex properties, as described in Manual Proof Using Coq
7.9.3.1. Manual Proof Using SPARK Lemma Library
If the property to prove is part of the SPARK Lemma Library, then manual
proof simply consists in calling the appropriate lemma in your code. For
example, consider the following assertion to prove, where X1, X2 and
Y may be signed or modular positive integers:
R1 := X1 / Y;
R2 := X2 / Y;
pragma Assert (R1 <= R2);
The property here is the monotonicity of division on positive values. There is a corresponding lemma for both signed and modular integers, for both 32 bits and 64 bits integers:
for signed 32 bits integers, use
SPARK.Integer_Arithmetic_Lemmas.Lemma_Div_Is_Monotonicfor signed 64 bits integers, use
SPARK.Long_Integer_Arithmetic_Lemmas.Lemma_Div_Is_Monotonicfor modular 32 bits integers, use
SPARK.Mod32_Arithmetic_Lemmas.Lemma_Div_Is_Monotonicfor modular 64 bits integers, use
SPARK.Mod64_Arithmetic_Lemmas.Lemma_Div_Is_Monotonic
For example, the lemma for signed integers has the following signature:
procedure Lemma_Div_Is_Monotonic
(Val1 : Int;
Val2 : Int;
Denom : Pos)
with
Global => null,
Pre => Val1 <= Val2,
Post => Val1 / Denom <= Val2 / Denom;
Assuming the appropriate library unit is with’ed and used in your code (see
SPARK Lemma Library for details), using the lemma is simply a call to
the ghost procedure Lemma_Div_Is_Monotonic:
R1 := X1 / Y;
R2 := X2 / Y;
Lemma_Div_Is_Monotonic (X1, X2, Y);
-- at this program point, the prover knows that R1 <= R2
-- the following assertion is proved automatically:
pragma Assert (R1 <= R2);
Note that the lemma may have a precondition, stating in which contexts the
lemma holds, which you will need to prove when calling it. For example, a
precondition check is generated in the code above to show that X1 <=
X2. Similarly, the types of parameters in the lemma may restrict the contexts
in which the lemma holds. For example, the type Pos for parameter Denom
of Lemma_Div_Is_Monotonic is the type of positive integers. Hence, a range
check may be generated in the code above to show that Y is positive.
To apply lemmas to signed or modular integers of different types than the ones used in the instances provided in the library, just convert the expressions passed in arguments, as follows:
R1 := X1 / Y;
R2 := X2 / Y;
Lemma_Div_Is_Monotonic (Integer(X1), Integer(X2), Integer(Y));
-- at this program point, the prover knows that R1 <= R2
-- the following assertion is proved automatically:
pragma Assert (R1 <= R2);
7.9.3.2. Manual Proof Using User Lemmas
If the property to prove is not part of the SPARK Lemma Library, then a user can easily add it as a separate lemma in her program. For example, suppose you need to have a proof that a fix list of numbers are prime numbers. This can be expressed easily in a lemma as follows:
function Is_Prime (N : Positive) return Boolean is
(for all J in Positive range 2 .. N - 1 => N mod J /= 0);
procedure Number_Is_Prime (N : Positive)
with
Ghost,
Global => null,
Pre => N in 15486209 | 15487001 | 15487469,
Post => Is_Prime (N);
Using the lemma is simply a call to the ghost procedure Number_Is_Prime:
Number_Is_Prime (15486209);
-- at this program point, the prover knows that 15486209 is prime, so
-- the following assertion is proved automatically:
pragma Assert (Is_Prime (15486209));
Note that the lemma here has a precondition, which you will need to prove when calling it. For example, the following incorrect call to the lemma will be detected as a precondition check failure:
Number_Is_Prime (10); -- check message issued here
Then, the lemma procedure can be either implemented as a null procedure, in which case GNATprove will issue a check message about the unproved postcondition, which can be justified (see Justifying Check Messages) or proved with Coq (see Manual Proof Using Coq):
procedure Number_Is_Prime (N : Positive) is null;
Or it can be implemented as a normal procedure body with a single assumption:
procedure Number_Is_Prime (N : Positive) is
begin
pragma Assume (Is_Prime (N));
end Number_Is_Prime;
Or it can be implemented in some cases as a normal procedure body with ghost code to achieve fully automatic proof, see Manual Proof Using Ghost Code.
7.9.3.3. Manual Proof Using Ghost Code
Guiding automatic solvers by adding intermediate assertions is a commonly used technique. More generally, whole pieces of Ghost Code can be added to enhance automated reasoning.
Proving Existential Quantification
Existentially quantified properties are difficult to verify for automatic solvers. Indeed, it requires coming up with a concrete value for which the property holds and solvers are not good at guessing. As an example, consider the following program:
type Nat_Array is array (Positive range <>) of Natural;
pragma Assume (A (A'First) = 0 and then A (A'Last) > 0);
pragma Assert
(for some I in A'Range =>
I < A'Last and then A (I) = 0 and then A (I + 1) > 0);
Here we assume that the first element of an array A of type Nat_Array
is 0, whereas is last element is positive. In such a case, we are sure that
there is an index I in the array such A (I) is 0 but not A (I + 1).
Indeed, we know that A starts with a non-empty sequence of zeros. The last
element of this sequence has the expected property. However, automatic solvers
are unable to prove such a property automatically because they cannot guess
which index they should consider.
To help them, we can define a ghost function returning a value for which the
property holds, and call it from an assertion:
type Nat_Array is array (Positive range <>) of Natural;
function Find_Pos (A : Nat_Array) return Positive with Ghost,
Pre => A (A'First) = 0 and then A (A'Last) > 0,
Post => Find_Pos’Result in A'First .. A'Last - 1 and then
A (Find_Pos'Result) = 0 and then A (Find_Pos'Result + 1) > 0;
pragma Assume (A (A'First) = 0 and then A (A'Last) > 0);
pragma Assert (Find_Pos (A) in A'Range);
pragma Assert
(for some I in A'Range =>
I < A'Last and then A (I) = 0 and then A (I + 1) > 0);
Automatic solvers are now able to discharge the proof.
Performing Induction
Another difficult point for automated solvers is proof by induction. Though
some automatic solvers do have heuristics allowing them to perform the most
simple inductive proofs, they generally are lost when the induction is less
straightforward. For example, in the example below, we state that the array
A is sorted in two different ways, first by saying that each element is
bigger than the one just before, and then by saying that each element is
bigger than all the ones before:
pragma Assume
(for all I in A'Range =>
(if I > A'First then A (I) > A (I - 1)));
pragma Assert
(for all I in A'Range =>
(for all J in A'Range => (if I > J then A (I) > A (J))));
The second assertion is provable from the first one by induction over the
number of elements separating I and J, but automatic solvers are unable
to verify this code. To help them, we can use a ghost loop. In the loop
invariant, we say that the property holds for all indexes I and J
separated by less than K elements:
procedure Prove_Sorted (A : Nat_Array) with Ghost is
begin
for K in 0 .. A'Length loop
pragma Loop_Invariant
(for all I in A'Range => (for all J in A'Range =>
(if I > J and then I - J <= K then A (I) > A (J))));
end loop;
end Prove_Sorted;
GNATprove will verify that the invariant holds in two steps, first it will show that the property holds at the first iteration, and then that, if it holds at a given iteration, then it also holds at the next (see Loop Invariants). Both proofs are straightforward using the assumption.
Note that we have introduced a ghost subprogram above to contain the loop. This will allow the compiler to recognize that this loop is ghost, so that it can be entirely removed when assertions are disabled.
If Prove_Sorted is declared locally to the subprogram that we want to
verify, it is not necessary to supply a contract for it, as local subprograms
with no contracts are inlined (see Contextual Analysis of Subprograms Without Contracts). We can still choose to provide such a contract to turn
Prove_Sorted into a lemma (see Manual Proof Using User Lemmas).
A Concrete Example: a Sort Algorithm
We show how to prove the correctness of a sorting procedure on arrays using ghost code. In particular, we want to show that the sorted array is a permutation of the input array. A common way to define permutations is to encode the number of occurrences of each element in the array as a multiset, constructed inductively over the size of its array parameter (but it is not the only one, see Ghost Variables). The Functional Containers Library of SPARK provides an implementation of multisets that we use here:
1pragma SPARK_Mode (On);
2
3with SPARK.Containers.Functional.Multisets;
4
5package Nat_Multisets is new SPARK.Containers.Functional.Multisets (Natural, "=");
1package Sort_Types with SPARK_Mode is
2 subtype Index is Integer range 1 .. 100;
3 type Nat_Array is array (Index range <>) of Natural;
4end Sort_Types;
1with SPARK.Big_Integers; use SPARK.Big_Integers;
2with Nat_Multisets; use Nat_Multisets;
3with Sort_Types; use Sort_Types;
4
5package Perm with SPARK_Mode, Ghost is
6 use Nat_Multisets;
7
8 function Occurrences (Values : Nat_Array; Lst : Integer) return Multiset is
9 (if Lst < Values'First then Empty_Multiset
10 else Add (Occurrences (Values, Lst - 1), Values (Lst)))
11 with Subprogram_Variant => (Decreases => Lst),
12 Pre => Lst <= Values'Last;
13
14 function Occurrences (Values : Nat_Array) return Multiset is
15 (Occurrences (Values, Values'Last));
16
17 function Occ (Values : Nat_Array; N : Natural) return Big_Natural is
18 (Nb_Occurence (Occurrences (Values), N));
19
20 function Is_Perm (Left, Right : Nat_Array) return Boolean is
21 (Occurrences (Left) = Occurrences (Right));
22
23end Perm;
The only property of the function Occurrences required to prove that
swapping two elements of an array is in fact a permutation, is the way
Occurrences is modified when updating a value of the array.
There is no native construction for axioms in SPARK. As a workaround, a
ghost subprogram, named “lemma subprogram”, can be introduced with the desired
property as a postcondition. An instance of the axiom will then be available
whenever the subprogram is called. Notice that an explicit call to the lemma
subprogram with the proper arguments is required whenever an instance of the
axiom is needed, like in manual proofs in an interactive theorem prover. Here
is how a lemma subprogram can be defined for the desired property of
Occurrences:
package Perm.Lemma_Subprograms with
SPARK_Mode,
Ghost,
Always_Terminates
is
function Is_Set (A : Nat_Array; I : Index; V : Natural; R : Nat_Array)
return Boolean
is (R'First = A'First and then R'Last = A'Last
and then R (I) = V
and then (for all J in A'Range =>
(if I /= J then R (J) = A (J)))) with
Pre => I in A'Range;
procedure Occ_Set (A : Nat_Array; I : Index; V : Natural; R : Nat_Array)
with
Global => null,
Pre => I in A'Range and then Is_Set (A, I, V, R),
Post =>
(if V = A (I) then Occurrences (R) = Occurrences (A)
else Occ (R, V) = Occ (A, V) + 1
and then Occ (R, A (I)) = Occ (A, A (I)) - 1
and then
(for all E of Union (Occurrences (R), Occurrences (A)) =>
(if E not in V | A (I) then Occ (R, E) = Occ (A, E))));
end Perm.Lemma_Subprograms;
This “axiom” can then be used to prove an implementation of the selection sort algorithm. The lemma subprogram needs to be explicitely called when needed:
with Nat_Multisets; use Nat_Multisets;
with Perm.Lemma_Subprograms; use Perm.Lemma_Subprograms;
package body Sort
with SPARK_Mode
is
-----------------------------------------------------------------------------
procedure Swap (Values : in out Nat_Array;
X : in Positive;
Y : in Positive)
with
Pre => (X in Values'Range and then
Y in Values'Range and then
X /= Y),
Post => Is_Perm (Values'Old, Values)
and Values (X) = Values'Old (Y)
and Values (Y) = Values'Old (X)
and (for all Z in Values'Range =>
(if Z /= X and Z /= Y then Values (Z) = Values'Old (Z)))
is
Temp : Integer;
-- Ghost variables
Init : constant Nat_Array (Values'Range) := Values with Ghost;
Interm : Nat_Array (Values'Range) with Ghost;
-- Ghost procedure
procedure Prove_Perm with Ghost,
Pre => X in Values'Range and then Y in Values'Range and then
Is_Set (Init, X, Init (Y), Interm)
and then Is_Set (Interm, Y, Init (X), Values),
Post => Is_Perm (Init, Values)
is
begin
Occ_Set (Init, X, Init (Y), Interm);
Occ_Set (Interm, Y, Init (X), Values);
pragma Assert
(for all F of Union (Occurrences (Init), Occurrences (Values)) =>
Occ (Values, F) = Occ (Init, F));
end Prove_Perm;
begin
Temp := Values (X);
Values (X) := Values (Y);
-- Ghost code
pragma Assert (Is_Set (Init, X, Init (Y), Values));
Interm := Values;
Values (Y) := Temp;
-- Ghost code
pragma Assert (Is_Set (Interm, Y, Init (X), Values));
Prove_Perm;
end Swap;
-- Finds the index of the smallest element in the array
function Index_Of_Minimum (Values : in Nat_Array)
return Positive
with
Pre => Values'Length > 0,
Post => Index_Of_Minimum'Result in Values'Range and then
(for all I in Values'Range =>
Values (Index_Of_Minimum'Result) <= Values (I))
is
Min : Positive;
begin
Min := Values'First;
for Index in Values'Range loop
if Values (Index) < Values (Min) then
Min := Index;
end if;
pragma Loop_Invariant
(Min in Values'Range and then
(for all I in Values'First .. Index =>
Values (Min) <= Values (I)));
end loop;
return Min;
end Index_Of_Minimum;
procedure Selection_Sort (Values : in out Nat_Array) is
Smallest : Positive; -- Index of the smallest value in the unsorted part
begin
if Values'Length = 0 then
return;
end if;
for Current in Values'First .. Values'Last - 1 loop
Smallest := Index_Of_Minimum (Values (Current .. Values'Last));
if Smallest /= Current then
Swap (Values => Values,
X => Current,
Y => Smallest);
end if;
pragma Loop_Invariant
(for all I in Values'First .. Current =>
(for all J in I + 1 .. Values'Last =>
Values (I) <= Values (J)));
pragma Loop_Invariant (Is_Perm (Values'Loop_Entry, Values));
end loop;
end Selection_Sort;
end Sort;
with SPARK.Big_Integers; use SPARK.Big_Integers;
with Sort_Types; use Sort_Types;
with Perm; use Perm;
package Sort with SPARK_Mode is
-- Sorts the elements in the array Values in ascending order
procedure Selection_Sort (Values : in out Nat_Array)
with
Post => Is_Perm (Values'Old, Values) and then
(if Values'Length > 0 then
(for all I in Values'First .. Values'Last - 1 =>
Values (I) <= Values (I + 1)));
end Sort;
The procedure Selection_Sort can be verified using GNATprove at level 2.
info: postcondition proved
--> sort.adb:18:16
info: index check proved
--> sort.adb:19:18
info: index check proved
--> sort.adb:19:35
info: index check proved
--> sort.adb:20:18
info: index check proved
--> sort.adb:20:35
info: index check proved
--> sort.adb:22:48
info: index check proved
--> sort.adb:22:65
info: initialization of "Temp" proved
--> sort.adb:24:07
info: range check proved
--> sort.adb:27:07
info: length check proved
--> sort.adb:27:53
info: initialization of "Interm" proved
--> sort.adb:28:07
info: range check proved
--> sort.adb:28:07
info: precondition proved
--> sort.adb:33:09
info: range check proved
--> sort.adb:33:23
info: index check proved
--> sort.adb:33:32
info: precondition proved
--> sort.adb:34:18
info: range check proved
--> sort.adb:34:34
info: index check proved
--> sort.adb:34:43
info: postcondition proved
--> sort.adb:35:17
info: precondition proved
--> sort.adb:38:10
info: range check proved
--> sort.adb:38:25
info: index check proved
--> sort.adb:38:34
info: precondition proved
--> sort.adb:39:10
info: range check proved
--> sort.adb:39:27
info: index check proved
--> sort.adb:39:36
info: assertion proved
--> sort.adb:41:13
info: predicate check proved
--> sort.adb:42:17
info: predicate check proved
--> sort.adb:42:35
info: index check proved
--> sort.adb:46:29
info: index check proved
--> sort.adb:47:15
info: index check proved
--> sort.adb:47:29
info: precondition proved
--> sort.adb:50:22
info: assertion proved
--> sort.adb:50:22
info: range check proved
--> sort.adb:50:36
info: index check proved
--> sort.adb:50:45
info: length check proved
--> sort.adb:51:14
info: length check proved
--> sort.adb:51:17
info: index check proved
--> sort.adb:53:15
info: range check proved
--> sort.adb:53:21
info: precondition proved
--> sort.adb:56:22
info: assertion proved
--> sort.adb:56:22
info: range check proved
--> sort.adb:56:38
info: index check proved
--> sort.adb:56:47
info: precondition proved
--> sort.adb:57:07
info: implicit aspect Always_Terminates on "Index_Of_Minimum" has been proved, subprogram will terminate
--> sort.adb:61:13
info: postcondition proved
--> sort.adb:65:16
info: index check proved
--> sort.adb:67:35
info: index check proved
--> sort.adb:67:55
info: initialization of "Min" proved
--> sort.adb:69:07
info: range check proved
--> sort.adb:71:20
info: index check proved
--> sort.adb:73:38
info: range check proved
--> sort.adb:74:20
info: loop invariant initialization proved
--> sort.adb:77:13
info: loop invariant preservation proved
--> sort.adb:77:13
info: index check proved
--> sort.adb:79:28
info: index check proved
--> sort.adb:79:44
info: initialization of "Smallest" proved
--> sort.adb:85:07
info: overflow check proved
--> sort.adb:91:50
info: precondition proved
--> sort.adb:92:22
info: range check proved
--> sort.adb:92:40
info: precondition proved
--> sort.adb:95:13
info: range check proved
--> sort.adb:96:29
info: loop invariant initialization proved
--> sort.adb:101:13
info: loop invariant preservation proved
--> sort.adb:101:13
info: overflow check proved
--> sort.adb:102:31
info: index check proved
--> sort.adb:103:28
info: index check proved
--> sort.adb:103:42
info: loop invariant initialization proved
--> sort.adb:104:33
info: loop invariant preservation proved
--> sort.adb:104:33
info: postcondition proved
--> sort.ads:10:16
info: overflow check proved
--> sort.ads:12:51
info: index check proved
--> sort.ads:13:22
info: overflow check proved
--> sort.ads:13:38
info: index check proved
--> sort.ads:13:38
To complete the verification of our selection sort, the only remaining issue
is the correctness of the axiom for Occurrences. It can be discharged using
its definition. Since this definition is recursive, the proof requires
induction, which is not normally in the reach of an automated prover. For
GNATprove to verify it, it must be implemented using recursive calls on
itself to assert the induction hypothesis. Note that the proof of the
lemma is then conditioned to the termination of the lemma functions, which
can be verified by GNATprove using a Subprogram Variant.
package body Perm.Lemma_Subprograms with SPARK_Mode is
procedure Occ_Eq (A, B : Nat_Array; LA, LB : Integer) with
Subprogram_Variant => (Decreases => LA),
Pre => LA <= A'Last and then LB <= B'Last
and then A (A'First .. LA) = B (B'First .. LB),
Post => Occurrences (A, LA) = Occurrences (B, LB);
procedure Occ_Eq (A, B : Nat_Array; LA, LB : Integer) is
begin
if LA < A'First then
return;
end if;
Occ_Eq (A, B, LA - 1, LB - 1);
end Occ_Eq;
procedure Occ_Set_Rec
(A : Nat_Array; I : Index; V : Natural; R : Nat_Array; L : Integer)
with
Subprogram_Variant => (Decreases => L),
Pre => I in A'Range and then Is_Set (A, I, V, R) and then L <= A'Last,
Post =>
(if V = A (I) or else I > L then Occurrences (R, L) = Occurrences (A, L)
else Nb_Occurence (Occurrences (R, L), V) =
Nb_Occurence (Occurrences (A, L), V) + 1
and then Nb_Occurence (Occurrences (R, L), A (I)) =
Nb_Occurence (Occurrences (A, L), A (I)) - 1
and then
(for all E of Occurrences (R, L) =>
(if E not in V | A (I)
then Nb_Occurence (Occurrences (R, L), E) =
Nb_Occurence (Occurrences (A, L), E)))
and then
(for all E of Occurrences (A, L) =>
(if E not in V | A (I)
then Nb_Occurence (Occurrences (R, L), E) =
Nb_Occurence (Occurrences (A, L), E))));
procedure Occ_Set_Rec
(A : Nat_Array; I : Index; V : Natural; R : Nat_Array; L : Integer)
is
begin
if L < A'First then
return;
end if;
if I = L then
Occ_Eq (A, R, L - 1, L - 1);
else
Occ_Set_Rec (A, I, V, R, L - 1);
end if;
end Occ_Set_Rec;
procedure Occ_Set (A : Nat_Array; I : Index; V : Natural; R : Nat_Array)
is
begin
Occ_Set_Rec (A, I, V, R, A'Last);
end Occ_Set;
end Perm.Lemma_Subprograms;
GNATprove proves automatically all checks on the final program at level 2.
info: implicit aspect Always_Terminates on "Occurrences" has been proved, subprogram will terminate
--> perm.ads:8:13
info: precondition proved
--> perm.ads:10:17
info: subprogram variant proved
--> perm.ads:10:17
info: overflow check proved
--> perm.ads:10:42
info: index check proved
--> perm.ads:10:56
info: implicit aspect Always_Terminates on "Occurrences" has been proved, subprogram will terminate
--> perm.ads:14:13
info: precondition proved
--> perm.ads:15:07
info: implicit aspect Always_Terminates on "Occ" has been proved, subprogram will terminate
--> perm.ads:17:13
info: implicit aspect Always_Terminates on "Is_Perm" has been proved, subprogram will terminate
--> perm.ads:20:13
info: aspect Always_Terminates on "Occ_Eq" has been proved, subprogram will terminate
--> perm-lemma_subprograms.adb:3:14
info: range check proved
--> perm-lemma_subprograms.adb:6:15
info: range check proved
--> perm-lemma_subprograms.adb:6:35
info: precondition proved
--> perm-lemma_subprograms.adb:7:14
info: postcondition proved
--> perm-lemma_subprograms.adb:7:14
info: precondition proved
--> perm-lemma_subprograms.adb:7:36
info: precondition proved
--> perm-lemma_subprograms.adb:15:07
info: subprogram variant proved
--> perm-lemma_subprograms.adb:15:07
info: overflow check proved
--> perm-lemma_subprograms.adb:15:24
info: overflow check proved
--> perm-lemma_subprograms.adb:15:32
info: aspect Always_Terminates on "Occ_Set_Rec" has been proved, subprogram will terminate
--> perm-lemma_subprograms.adb:18:14
info: precondition proved
--> perm-lemma_subprograms.adb:22:36
info: postcondition proved
--> perm-lemma_subprograms.adb:24:08
info: index check proved
--> perm-lemma_subprograms.adb:24:19
info: precondition proved
--> perm-lemma_subprograms.adb:24:41
info: precondition proved
--> perm-lemma_subprograms.adb:24:62
info: predicate check proved
--> perm-lemma_subprograms.adb:25:14
info: precondition proved
--> perm-lemma_subprograms.adb:25:28
info: predicate check proved
--> perm-lemma_subprograms.adb:26:11
info: precondition proved
--> perm-lemma_subprograms.adb:26:25
info: predicate check proved
--> perm-lemma_subprograms.adb:26:50
info: predicate check proved
--> perm-lemma_subprograms.adb:27:18
info: precondition proved
--> perm-lemma_subprograms.adb:27:32
info: index check proved
--> perm-lemma_subprograms.adb:27:55
info: predicate check proved
--> perm-lemma_subprograms.adb:28:11
info: precondition proved
--> perm-lemma_subprograms.adb:28:25
info: index check proved
--> perm-lemma_subprograms.adb:28:48
info: predicate check proved
--> perm-lemma_subprograms.adb:28:54
info: precondition proved
--> perm-lemma_subprograms.adb:30:25
info: index check proved
--> perm-lemma_subprograms.adb:31:34
info: predicate check proved
--> perm-lemma_subprograms.adb:32:20
info: precondition proved
--> perm-lemma_subprograms.adb:32:34
info: predicate check proved
--> perm-lemma_subprograms.adb:33:17
info: precondition proved
--> perm-lemma_subprograms.adb:33:31
info: precondition proved
--> perm-lemma_subprograms.adb:35:25
info: index check proved
--> perm-lemma_subprograms.adb:36:34
info: predicate check proved
--> perm-lemma_subprograms.adb:37:20
info: precondition proved
--> perm-lemma_subprograms.adb:37:34
info: predicate check proved
--> perm-lemma_subprograms.adb:38:17
info: precondition proved
--> perm-lemma_subprograms.adb:38:31
info: precondition proved
--> perm-lemma_subprograms.adb:49:10
info: overflow check proved
--> perm-lemma_subprograms.adb:49:26
info: overflow check proved
--> perm-lemma_subprograms.adb:49:33
info: precondition proved
--> perm-lemma_subprograms.adb:51:10
info: subprogram variant proved
--> perm-lemma_subprograms.adb:51:10
info: overflow check proved
--> perm-lemma_subprograms.adb:51:37
info: precondition proved
--> perm-lemma_subprograms.adb:58:07
info: implicit aspect Always_Terminates on "Is_Set" has been proved, subprogram will terminate
--> perm-lemma_subprograms.ads:7:13
info: index check proved
--> perm-lemma_subprograms.ads:10:20
info: index check proved
--> perm-lemma_subprograms.ads:12:39
info: index check proved
--> perm-lemma_subprograms.ads:12:47
info: aspect Always_Terminates on "Occ_Set" has been proved, subprogram will terminate
--> perm-lemma_subprograms.ads:15:14
info: data dependencies proved
--> perm-lemma_subprograms.ads:17:06
info: precondition proved
--> perm-lemma_subprograms.ads:18:38
info: postcondition proved
--> perm-lemma_subprograms.ads:20:08
info: index check proved
--> perm-lemma_subprograms.ads:20:19
info: predicate check proved
--> perm-lemma_subprograms.ads:21:14
info: predicate check proved
--> perm-lemma_subprograms.ads:21:27
info: predicate check proved
--> perm-lemma_subprograms.ads:21:40
info: predicate check proved
--> perm-lemma_subprograms.ads:22:20
info: index check proved
--> perm-lemma_subprograms.ads:22:31
info: predicate check proved
--> perm-lemma_subprograms.ads:22:37
info: index check proved
--> perm-lemma_subprograms.ads:22:48
info: predicate check proved
--> perm-lemma_subprograms.ads:22:54
info: index check proved
--> perm-lemma_subprograms.ads:25:36
info: predicate check proved
--> perm-lemma_subprograms.ads:25:44
info: predicate check proved
--> perm-lemma_subprograms.ads:25:57
7.9.3.4. Manual Proof Using Coq
This section presents a simple example of how to prove interactively a check with an interactive prover like Coq when GNATprove fails to prove it automatically (for installation of Coq, see also: Coq). Here is a simple SPARK procedure:
1procedure Nonlinear (X, Y, Z : Positive; R1, R2 : out Natural) with
2 SPARK_Mode,
3 Pre => Y > Z,
4 Post => R1 <= R2
5is
6begin
7 R1 := X / Y;
8 R2 := X / Z;
9end Nonlinear;
When only the Alt-Ergo prover is used, GNATprove does not prove automatically the postcondition of the procedure, even when increasing the value of the timeout:
medium: postcondition might fail
--> nonlinear.adb:4:11
4 | Post => R1 <= R2
| ^~~~~~~~
This is expected, as the automatic prover Alt-Ergo has only a simple support
for non-linear integer arithmetic. More generally, it is a known difficulty for
all automatic provers, although, in the case above, using prover cvc5 is enough
to prove automatically the postcondition of procedure Nonlinear. We will
use this case to demonstrate the use of a manual prover, as an example of what
can be done when automatic provers fail to prove a check. We will use Coq here.
The Coq input file associated to this postcondition can be produced by either
selecting and specifying Coq as
alternate prover in GNAT Studio or by executing on the command-line:
gnatprove -P <prj_file>.gpr --limit-line=nonlinear.adb:4:11:VC_POSTCONDITION --prover=Coq
The generated file contains many definitions and axioms that can be used in the proof, in addition to the ones in Coq standard library. The property we want to prove is at the end of the file:
Theorem def'vc :
forall (r1:Numbers.BinNums.Z) (r2:Numbers.BinNums.Z),
dynamic_invariant1 x Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant1 y Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant1 z Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant r1 Init.Datatypes.false Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant r2 Init.Datatypes.false Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true -> (z < y)%Z ->
forall (r11:Numbers.BinNums.Z), (r11 = (ZArith.BinInt.Z.quot x y)) ->
forall (r21:Numbers.BinNums.Z), (r21 = (ZArith.BinInt.Z.quot x z)) ->
(r11 <= r21)%Z.
Proof.
intros r1 r2 h1 h2 h3 h4 h5 h6 r11 h7 r21 h8.
Qed.
From the forall to the first . we can see the expression of what must
be proved, also called the goal. The proof starts right after the dot and ends
with the Qed keyword. Proofs in Coq are done with the help of different
tactics which will change the state of the current goal. The first tactic
(automatically added) here is intros, which allows to “extract” variables
and hypotheses from the current goal and add them to the current
environment. Each parameter to the intros tactic is the name that the
extracted element will have in the new environment. The intros tactic here
puts all universally quantified variables and all hypotheses in the
environment. The goal is reduced to a simple inequality, with all potentially
useful information in the environment.
Here is the state of the proof as displayed in a suitable IDE for Coq:
1 subgoal
r1, r2 : int
h1 : dynamic_invariant1 x true false true true
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
r11 : int
h7 : r11 = (x ÷ y)%Z
r21 : int
h8 : r21 = (x ÷ z)%Z
______________________________________(1/1)
(r11 <= r21)%Z
Some expresions are enclosed in ()%Z, which means that they are dealing
with relative integers. This is necessarily in order to use the operators
(e.g. < or +) on relative integers instead of using the associated Coq
function or to declare a relative integer constant (e.g. 0%Z).
Next, we can use the subst tactic to automaticaly replace variables by
terms to which they are equal (as stated by the hypotheses in the current
environment) and clean the environment of replaced variables. Here, we can get
rid of many variables at once with subst. (note the presence of the .
at the end of each tactic). The new state is:
1 subgoal
r1, r2 : int
h1 : dynamic_invariant1 x true false true true
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/1)
(x ÷ y <= x ÷ z)%Z
At this state, the hypotheses alone are not enough to prove the goal without
proving properties about ÷ and < operators. It is necessary to use
theorems from the Coq standard library. Coq provides a command SearchAbout
to find theorems and definition concerning its argument. For instance, to find
the theorems referring to the operator ÷, we use SearchAbout Z.quot.,
where Z.quot is the underlying function for the ÷ operator. Among the
theorems displayed, the conclusion (the rightmost term separated by ->
operator) of one of them seems to match our current goal:
Z.quot_le_compat_l:
forall p q r : int, (0 <= p)%Z -> (0 < q <= r)%Z -> (p ÷ r <= p ÷ q)%Z
The tactic apply allows the use of a theorem or an hypothesis on the
current goal. Here we use: apply Z.quot_le_compat_l.. This tactic will try
to match the different variables of the theorem with the terms present in the
goal. If it succeeds, one subgoal per hypothesis in the theorem will be
generated to verify that the terms matched with the theorem variables satisfy
the hypotheses on those variables required by the theorem. In this
case, p is matched with x, q with z and
r with y and the new state is:
2 subgoals
r1, r2 : int
h1 : dynamic_invariant1 x true false true true
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/2)
(0 <= x)%Z
______________________________________(2/2)
(0 < z <= y)%Z
As expected, there are two subgoals, one per hypothesis of the theorem. Once
the first subgoal is proved, the rest of the script will automatically apply to
the second one. Now, if we look back at the SPARK code, X is of type
Positive so X is greater than 0 and dynamic_invariantN (where N is
a number) are predicates generated by SPARK to state the range of a value
from a ranged subtype interpreted as a relative integer in Coq. Here, the
predicate dynamic_invariant1 provides the property needed to prove the first
subgoal which is that “All elements of subtype positive have their integer
interpretation in the range 1 .. (2³¹ - 1)”. To be able to see the definition
of dynamic_invariant1 in h1, we can use the unfold tactic of Coq. We
need to supply the name of the predicate to unfold:
unfold dynamic_invariant1 in h1. After this unfolding, we get a new
predicate in_range1 that we can unfold too so that h1 is now
true = true \/ (1 <= 2147483647)%Z -> (1 <= x <= 2147483647)%Z.
We see now that the goal does not match exactly the hypothesis, because one is a comparison with 0, while the other is a comparison with 1. Transitivity on “lesser or equal” relation is needed to prove this goal, of course this is provided in Coq’s standard library:
Lemma Z.le_trans : forall n m p:Z, (n <= m)%Z -> (m <= p)%Z -> (n <= p)%Z.
Since the lemma’s conclusion contains only two variables while it uses three,
using tactic apply Z.le_trans. will generate an error stating that Coq was
not able to find a term for the variable m. In this case, m needs to
be instantiated explicitly, here with the value 1: apply Zle_trans with (m:=
1%Z). There are two new subgoals, one to prove that 0 <= 1 and the other
that 1 <= x:
3 subgoals
r1, r2 : int
h1 : true = true \/ (1 <= 2147483647)%Z -> (1 <= x <= 2147483647)%Z
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/3)
(0 <= 1)%Z
______________________________________(2/3)
(1 <= x)%Z
______________________________________(3/3)
(0 < z <= y)%Z
To prove that 0 <= 1, the theorem Lemma Z.le_0_1 : (0 <= 1)%Z. is used.
apply Z.le_0_1 will not generate any new subgoals since it does not contain
implications. Coq passes to the next subgoal:
2 subgoals
r1, r2 : int
h1 : true = true \/ (1 <= 2147483647)%Z -> (1 <= x <= 2147483647)%Z
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/2)
(1 <= x)%Z
______________________________________(2/2)
(0 < z <= y)%Z
This goal is now adapted to the range information in hypothesis h1. It
introduces a subgoal which is the disjunction in the hypothesis of h1.
To prove this disjunction, we need to tell Coq which operand we want to prove.
Here, both are obviously true. Let’s choose the left one using the tactic
left.. We are left with only the equality to prove:
2 subgoals
r1, r2 : int
h1 : true = true \/ (1 <= 2147483647)%Z -> (1 <= x <= 2147483647)%Z
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/2)
true = true
______________________________________(2/2)
(0 < z <= y)%Z
This can be discharged using apply eq_refl. to apply the reflexivity
axiom of equality.
Now the subgoal 1 is fully proved, and all that remains
is subgoal 2:
1 subgoal
r1, r2 : int
h1 : dynamic_invariant1 x true false true true
h2 : dynamic_invariant1 y true false true true
h3 : dynamic_invariant1 z true false true true
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/1)
(0 < z <= y)%Z
Transitivity is needed again, as well as the definition of
dynamic_invariant1. In the previous
subgoal, every step was detailed in order to show how the tactic apply
worked. Now, let’s see that proof doesn’t have to be this detailed. The first
thing to do is to add the fact that 1 <= z to the current
environment: unfold dynamic_invariant1, in_range1 in h3. will add the range
of z as an hypthesis in the environment:
1 subgoal
r1, r2 : int
h1 : dynamic_invariant1 x true false true true
h2 : dynamic_invariant1 y true false true true
h3 : true = true \/ (1 <= 2147483647)%Z -> (1 <= z <= 2147483647)%Z
h4 : dynamic_invariant r1 false false true true
h5 : dynamic_invariant r2 false false true true
h6 : (z < y)%Z
______________________________________(1/1)
(0 < z <= y)%Z
At this point, the goal can be solved simply using the intuition. tactic.
intuition is an automatic tactic of Coq implementing a decision procedure
for some simple goals. It either solves the goal or, if it fails, it does not
generate any subgoals. The benefit of the latter way is that there are less
steps than with the previous subgoal for a more complicated goal (there are two
inequalities in the second subgoal) and we do not have to find the different
theorems we need to solve the goal without intuition.
Finally, here is the final version of the proof script for the postcondition:
Theorem def'vc :
forall (r1:Numbers.BinNums.Z) (r2:Numbers.BinNums.Z),
dynamic_invariant1 x Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant1 y Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant1 z Init.Datatypes.true Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant r1 Init.Datatypes.false Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true ->
dynamic_invariant r2 Init.Datatypes.false Init.Datatypes.false
Init.Datatypes.true Init.Datatypes.true -> (z < y)%Z ->
forall (r11:Numbers.BinNums.Z), (r11 = (ZArith.BinInt.Z.quot x y)) ->
forall (r21:Numbers.BinNums.Z), (r21 = (ZArith.BinInt.Z.quot x z)) ->
(r11 <= r21)%Z.
Proof.
intros r1 r2 h1 h2 h3 h4 h5 h6 r11 h7 r21 h8.
subst.
apply Z.quot_le_compat_l.
apply Z.le_trans with (m:=1%Z).
(* 0 <= x *)
- apply Z.le_0_1.
(* 1 <= x *)
- unfold dynamic_invariant1, in_range1 in h1.
apply h1. left. apply eq_refl.
(* 0 < z <= y *)
- unfold dynamic_invariant1, in_range1 in h3.
intuition.
Qed.
To check and save the proof:
gnatprove -P <prj_file>.gpr --limit-line=nonlinear.adb:4:11:VC_POSTCONDITION --prover=Coq --report=all
Now running GNATprove on the project should confirm that all checks are proved:
nonlinear.adb:4:11: info: postcondition proved
nonlinear.adb:7:12: info: range check proved
nonlinear.adb:7:12: info: division check proved
nonlinear.adb:8:12: info: range check proved
nonlinear.adb:8:12: info: division check proved