7.7. How to Write Loop Invariants
As described in Loop Invariants, proving properties of subprograms that contain loops may require the addition of explicit loop invariant contracts. This section describes a systematic approach for writing loop invariants.
7.7.1. Automatic Unrolling of Simple For-Loops
GNATprove automatically unrolls simple for-loops, defined as:
for-loops over a range,
with a number of iterations smaller than 20,
without Loop Invariants or Loop Variants,
that declare no local variables, or only variables of scalar type.
In addition, GNATprove always unrolls loops of the form for J in 1 .. 1
loop
that don’t have a Loop Invariants or Loop Variants, even
when they declare local variables of non-scalar type.
As a result of unrolling, GNATprove conveys the exact meaning of the loop to provers, without requiring a loop invariant. While this is quite powerful, it is best applied to loops where the body of the loop is small, otherwise the unrolling may lead to complex formulas that provers cannot prove.
For example, consider the subprograms Init
and Sum
below:
1package Loop_Unrolling with
2 SPARK_Mode
3is
4 subtype Index is Integer range 1 .. 10;
5 type Arr is array (Index) of Integer;
6
7 procedure Init (A : out Arr) with
8 Post => (for all J in Index => A(J) = J);
9
10 function Sum (A : Arr) return Integer with
11 Pre => (for all J in Index => A(J) = J),
12 Post => Sum'Result = (A'First + A'Last) * A'Length / 2;
13
14end Loop_Unrolling;
1package body Loop_Unrolling with
2 SPARK_Mode
3is
4 procedure Init (A : out Arr) is
5 begin
6 for J in Index loop
7 A (J) := J;
8 end loop;
9 end Init;
10
11 function Sum (A : Arr) return Integer is
12 Result : Integer := 0;
13 begin
14 for J in Index loop
15 Result := Result + A (J);
16 end loop;
17 return Result;
18 end Sum;
19
20end Loop_Unrolling;
As the loops in both subprograms are simple for-loops, GNATprove unrolls them
and manages to prove the postconditions of Init
and Sum
without
requiring a loop invariant:
1loop_unrolling.adb:15:27: info: overflow check proved
2loop_unrolling.ads:7:20: info: initialization of "A" proved
3loop_unrolling.ads:8:14: info: postcondition proved
4loop_unrolling.ads:10:13: info: implicit aspect Always_Terminates on "Sum" has been proved, subprogram will terminate
5loop_unrolling.ads:12:14: info: postcondition proved
Automatic loop unrolling can be disabled locally by explicitly adding a default loop invariant at the start of the loop:
for X in A .. B loop
pragma Loop_Invariant (True);
...
end loop;
It can also be disabled globally by using the switch --no-loop-unrolling
.
7.7.2. Automatically Generated Loop Invariants
In general, GNATprove relies on the user to manually supply the necessary information about variables modified by loop statements in the loop invariant. Though variables which are not modified in the loop need not be mentioned in the invariant, it is usually necessary to state explicitly the preservation of unmodified object parts, such as record or array components. In particular, when a loop modifies a collection, which can be either an array or a container (see Formal Containers Library), it may be necessary to state in the loop invariant those parts of the collection that have not been modified up to the current iteration. This property called frame condition in the scientific literature is essential for GNATprove, which otherwise must assume that all elements in the collection may have been modified. Special care should be taken to write adequate frame conditions, as they usually look obvious to programmers, and so it is very common to forget to write them and not being able to realize what’s the problem afterwards.
To alleviate this problem, the GNATprove tool generates automatically frame
conditions in some cases. As examples of use of such generated frame
conditions, consider the code of procedures Update_Arr
and Update_Rec
below:
1package Frame_Condition with
2 SPARK_Mode
3is
4 type Index is range 1 .. 100;
5 type Arr is array (Index) of Integer;
6
7 procedure Update_Arr (A : in out Arr; Idx : Index) with
8 Post => A(Idx + 1 .. A'Last) = A(Idx + 1 .. A'Last)'Old;
9
10 type Rec is record
11 A : Arr;
12 X : Integer;
13 end record;
14
15 procedure Update_Rec (R : in out Rec) with
16 Post => R.X = R.X'Old;
17
18end Frame_Condition;
1package body Frame_Condition with
2 SPARK_Mode
3is
4 procedure Update_Arr (A : in out Arr; Idx : Index) is
5 begin
6 for J in A'First .. Idx loop
7 A(J) := Integer(J);
8 end loop;
9 end Update_Arr;
10
11 procedure Update_Rec (R : in out Rec) is
12 begin
13 for J in R.A'Range loop
14 R.A(J) := Integer(J);
15 end loop;
16 end Update_Rec;
17
18end Frame_Condition;
Without this feature, GNATprove would not be able to prove the postconditions of either procedure because:
To prove the postcondition of
Update_Arr
, one needs to know that only the indexes up toIdx
have been updated in the loop.To prove the postcondition of
Update_Rec
, one needs to know that only the componentA
of recordR
has been updated in the loop.
Thanks to this feature, GNATprove automatically proves the postconditions of both procedures, without the need for loop invariants:
1frame_condition.ads:8:14: info: range check proved
2frame_condition.ads:8:14: info: postcondition proved
3frame_condition.ads:8:37: info: range check proved
4frame_condition.ads:16:14: info: postcondition proved
In particular, it is able to infer the preservation of unmodified components of record variables. It also handles unmodified components of array variables as long as they are preserved at every index in the array. As an example, consider the following loop which only updates some record component of a nested data structure:
1procedure Preserved_Fields with SPARK_Mode is
2 type R is record
3 F1 : Integer := 0;
4 F2 : Integer := 0;
5 end record;
6
7 type R_Array is array (1 .. 100) of R;
8
9 type R_Array_Record is record
10 F3 : R_Array;
11 F4 : R_Array;
12 end record;
13
14 D : R_Array_Record;
15
16begin
17 for I in 1 .. 100 loop
18 D.F3 (I).F1 := 0;
19 pragma Assert (for all J in 1 .. 100 =>
20 D.F3 (J).F2 = D.F3'Loop_Entry (J).F2);
21 pragma Assert (D.F4 = D.F4'Loop_Entry);
22 end loop;
23
24end Preserved_Fields;
Despite the absence of a loop invariant in the above code,
GNATprove is able to prove that the assertions on lines 19-21 about variable
D
which is modified in the loop are proved, thanks to the generated loop
invariants:
1preserved_fields.adb:14:04: info: initialization of "D" proved
2preserved_fields.adb:19:22: info: assertion proved
3preserved_fields.adb:21:22: info: assertion proved
Note that GNATprove will not generate a frame condition for a record component if the record variable is modified as a whole either through an assignment or through a procedure call, et cetera, even if the component happens to be preserved by the modification.
GNATprove can also infer preservation of unmodified array components for arrays that are only updated at constant indexes or at indexes equal to the loop index. As an example, consider the following loops, only updating some cells of a matrix of arrays:
1procedure Preserved_Components with SPARK_Mode is
2
3 type A is array (1 .. 100) of Natural with Default_Component_Value => 1;
4
5 type A_Matrix is array (1 .. 100, 1 .. 100) of A;
6
7 M : A_Matrix;
8
9begin
10 L1: for I in 1 .. 100 loop
11 M (I, 1) (1 .. 50) := (others => 0);
12 pragma Assert
13 (for all K1 in 1 .. 100 =>
14 (for all K2 in 1 .. 100 =>
15 (for all K3 in 1 .. 100 =>
16 (if K1 > I or else K2 /= 1 or else K3 > 50 then
17 M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
18 end loop L1;
19
20 L2: for I in 1 .. 99 loop
21 M (I + 1, I) (I .. 100) := (others => 0);
22 pragma Assert
23 (for all K1 in 1 .. 100 =>
24 (for all K2 in 1 .. 100 =>
25 (for all K3 in 1 .. 100 =>
26 (if K1 > I + 1 then
27 M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
28 pragma Assert
29 (for all K1 in 1 .. 100 =>
30 (for all K2 in 1 .. 100 =>
31 (for all K3 in 1 .. 100 =>
32 (if K3 < K2 then
33 M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
34 end loop L2;
35
36end Preserved_Components;
Despite the absence of a loop invariant in the above code, GNATprove can succesfully verify the assertion on line 13 thanks to the generated loop invariant. Note that loop invariant generation for preserved array components is based on heuristics, and that it is therefore far from complete. In particular, it does not handle updates to variable indexes different from the loop index, as can be seen by the failed attempt to verify the assertion on line 22. GNATprove does not either handle dependences between indexes in an update, resulting in the failed attempt to verify the assertion on line 33:
1preserved_components.adb:7:04: info: initialization of "M" proved
2preserved_components.adb:13:10: info: assertion proved
3preserved_components.adb:21:07: info: range check proved
4preserved_components.adb:21:21: info: index check proved
5preserved_components.adb:21:26: info: index check proved
6preserved_components.adb:21:31: info: length check proved
7preserved_components.adb:21:34: info: length check proved
8
9preserved_components.adb:27:30: medium: assertion might fail, cannot prove M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)
10 27 | M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
11 | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
12 possible fix: loop at line 20 should mention M in a loop invariant
13 20 | L2: for I in 1 .. 99 loop
14 | ^ here
15
16preserved_components.adb:33:30: medium: assertion might fail, cannot prove M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)
17 33 | M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
18 | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
19 possible fix: loop at line 20 should mention M in a loop invariant
20 20 | L2: for I in 1 .. 99 loop
21 | ^ here
7.7.3. The Four Properties of a Good Loop Invariant
A loop invariant can describe more or less precisely the behavior of a loop. What matters is that the loop invariant allows proving absence of run-time errors in the subprogram, that the subprogram respects its contract, and that the loop invariant itself holds at each iteration of the loop. There are four properties that a good loop invariant should fulfill:
[INIT] It should be provable in the first iteration of the loop.
[INSIDE] It should allow proving absence of run-time errors and local assertions inside the loop.
[AFTER] It should allow proving absence of run-time errors, local assertions and the subprogram postcondition after the loop.
[PRESERVE] It should be provable after the first iteration of the loop.
As a first example, here is a variant of the search algorithm described in SPARK Tutorial, which returns whether a collection contains a desired value, and if so, at which index. The collection is implemented as an array.
The specification of Linear_Search
is given in file linear_search.ads
.
The postcondition of Search
expresses that, either the search returns a
result within the array bounds, in which case it is the desired index,
otherwise the array does not contain the value searched.
1package Linear_Search
2 with SPARK_Mode
3is
4 type Opt_Index is new Natural;
5
6 subtype Index is Opt_Index range 1 .. Opt_Index'Last - 1;
7
8 No_Index : constant Opt_Index := 0;
9
10 type Ar is array (Index range <>) of Integer;
11
12 function Search (A : Ar; I : Integer) return Opt_Index with
13 Post => (if Search'Result in A'Range then A (Search'Result) = I
14 else (for all K in A'Range => A (K) /= I));
15
16end Linear_Search;
The implementation of Linear_Search
is given in file linear_search.adb
.
The loop invariant of Search
expresses that, at the end of each iteration,
if the loop has not been exited before, then the value searched is not in the
range of indexes between the start of the array A'First
and the current
index Pos
. The loop variant is used to prove termination of the loop.
1package body Linear_Search
2 with SPARK_Mode
3is
4
5 function Search (A : Ar; I : Integer) return Opt_Index is
6 begin
7 for Pos in A'Range loop
8 if A (Pos) = I then
9 return Pos;
10 end if;
11
12 pragma Loop_Invariant (for all K in A'First .. Pos => A (K) /= I);
13 end loop;
14
15 return No_Index;
16 end Search;
17
18end Linear_Search;
With this loop invariant, GNATprove is able to prove all checks in
Linear_Search
, both those related to absence of run-time errors and those
related to verification of contracts:
1linear_search.adb:9:20: info: range check proved
2linear_search.adb:12:33: info: loop invariant preservation proved
3linear_search.adb:12:33: info: loop invariant initialization proved
4linear_search.adb:12:67: info: index check proved
5linear_search.ads:12:13: info: implicit aspect Always_Terminates on "Search" has been proved, subprogram will terminate
6linear_search.ads:13:14: info: postcondition proved
7linear_search.ads:13:57: info: index check proved
8linear_search.ads:14:48: info: index check proved
In particular, the loop invariant fulfills all four properties that we listed above:
[INIT] It is proved in the first iteration (message on line 3).
[INSIDE] It allows proving absence of run-time errors inside the loop (messages on lines 1 and 4).
[AFTER] It allows proving absence of run-time errors after the loop (messages on lines 6 and 7) and the subprogram postcondition (message on line 5).
[PRESERVE] It is proved after the first iteration (message on line 2).
Note that the loop invariant closely resembles the second line in the
postcondition of the subprogram, except with a different range of values in the
quantification: instead of stating a property for all indexes in the array
A
, the loop invariant states the same property for all indexes up to the
current loop index Pos
. In fact, if we equate Pos
to A'Last
for the
last iteration of the loop, the two properties are equal. This explains here
how the loop invariant allows proving the subprogram postcondition when the
value searched is not found.
Note also that we chose to put the loop invariant at the end of the loop. We
could as easily put it at the start of the loop. In that case, the range of
values in the quantification should be modified to state that, at the start of
each iteration, if the loop has not been exited before, then the value searched
is not in the range of indexes between the start of the array A'First
and
the current index Pos
excluded:
pragma Loop_Invariant (for all K in A'First .. Pos - 1 => A (K) /= I);
Indeed, the test for the value at index Pos
is done after the loop
invariant in that case.
We will now demonstrate techniques to complete a loop invariant so that it fulfills all four properties [INIT], [INSIDE], [AFTER] and [PRESERVE], on a more complex algorithm searching in an ordered collection of elements. Like the naive search algorithm just described, this algorithm returns whether the collection contains the desired value, and if so, at which index. The collection is also implemented as an array.
The specification of this Binary_Search
is given in file binary_search.ads
:
1package Binary_Search
2 with SPARK_Mode
3is
4 type Opt_Index is new Natural;
5
6 subtype Index is Opt_Index range 1 .. Opt_Index'Last - 1;
7
8 No_Index : constant Opt_Index := 0;
9
10 type Ar is array (Index range <>) of Integer;
11
12 function Empty (A : Ar) return Boolean is (A'First > A'Last);
13
14 function Sorted (A : Ar) return Boolean is
15 (for all I1 in A'Range =>
16 (for all I2 in I1 .. A'Last => A (I1) <= A (I2)));
17
18 function Search (A : Ar; I : Integer) return Opt_Index with
19 Pre => Sorted (A),
20 Post => (if Search'Result in A'Range then A (Search'Result) = I
21 else (for all Index in A'Range => A (Index) /= I));
22
23end Binary_Search;
The implementation of Binary_Search
is given in file binary_search.adb
:
1package body Binary_Search
2 with SPARK_Mode
3is
4
5 function Search (A : Ar; I : Integer) return Opt_Index is
6 Left : Index;
7 Right : Index;
8 Med : Index;
9 begin
10 if Empty (A) then
11 return No_Index;
12 end if;
13
14 Left := A'First;
15 Right := A'Last;
16
17 if Left = Right and A (Left) = I then
18 return Left;
19 elsif A (Left) > I or A (Right) < I then
20 return No_Index;
21 end if;
22
23 while Left <= Right loop
24 pragma Loop_Variant (Increases => Left, Decreases => Right);
25
26 Med := Left + (Right - Left) / 2;
27
28 if A (Med) < I then
29 Left := Med + 1;
30 elsif A (Med) > I then
31 Right := Med - 1;
32 else
33 return Med;
34 end if;
35 end loop;
36
37 return No_Index;
38 end Search;
39
40end Binary_Search;
Note that, although function Search
has a loop, we have not given an
explicit loop invariant yet, so the default loop invariant of True
will be
used by GNATprove. We have added a loop variant to prove termination of the
function. We are running GNATprove with a prover timeout of 60 seconds
(switch --timeout=60
) to get the results presented in the rest of this
section.
7.7.4. Proving a Loop Invariant in the First Iteration
Property [INIT] is the easiest one to prove. This is equivalent to proving a pragma Assert in the sequence of statements obtained by unrolling the loop once. In particular, if the loop invariant is at the start of the loop, this is equivalent to proving a pragma Assert just before the loop. Therefore, the usual techniques for investigating unproved checks apply, see How to Investigate Unproved Checks.
7.7.5. Completing a Loop Invariant to Prove Checks Inside the Loop
Let’s start by running GNATprove on program Binary_Search
without loop
invariant. It generates two medium messages, one corresponding to a possible
run-time check failure, and one corresponding to a possible failure of
the postcondition:
binary_search.adb:28:16: medium: array index check might fail
28 | if A (Med) < I then
| ^~~
reason for check: value must be a valid index into the array
possible fix: loop at line 23 should mention Med in a loop invariant
23 | while Left <= Right loop
| ^ here
binary_search.ads:21:49: medium: postcondition might fail, cannot prove A (Index) /= I
21 | else (for all Index in A'Range => A (Index) /= I));
| ^~~~~~~~~~~~~~
We will focus here on the message inside the loop, which corresponds to
property [INSIDE]. The problem is that variable Med
varies in the loop, so
GNATprove only knows that its value is in the range of its type Index
at
the start of an iteration (line 23), and that it is then assigned the value of
Left + (Right - Left) / 2
(line 24) before being used as an index into
array A
(lines 26 and 28) and inside expressions assigned to Left
and
Right
(lines 27 and 29).
As Left
and Right
also vary in the loop, GNATprove cannot use the
assignment on line 24 to compute a more precise range for variable Med
,
hence the message on index check.
What is needed here is a loop invariant that states that the values of Left
and Right
stay within the bounds of A
inside the loop:
while Left <= Right loop
pragma Loop_Variant (Increases => Left, Decreases => Right);
pragma Loop_Invariant (Left in A'Range and Right in A'Range);
With this simple loop invariant, GNATprove now reports that the
check on line 26 is proved.
GNATprove computes that the value assigned to Med
in the loop is also
within the bounds of A
.
7.7.6. Completing a Loop Invariant to Prove Checks After the Loop
With the simple loop invariant given before, GNATprove still reports that the
postcondition of Search
may fail, which corresponds to property [AFTER]. By
instructing GNATprove to prove checks progressively, as seens in
Proving SPARK Programs, we even get a precise message pointing to the
part of the postcondition that could not be proved:
binary_search.ads:21:49: medium: postcondition might fail, cannot prove A (Index) /= I
21 | else (for all Index in A'Range => A (Index) /= I));
| ^~~~~~~~~~~~~~
Here, the message shows that the second line of the postcondition could not be
proved. This line expresses that, in the case where Search
returns
No_Index
after the loop, the array A
should not contain the value
searched I
.
One can very easily check that, if GNATprove can prove this property, it can also prove the postcondition. Simply insert a pragma Assert after the loop stating this property:
end if;
end loop;
pragma Assert (for all Index in A'Range => A (Index) /= I);
GNATprove now succeeds in proving the postcondition, but it fails to prove the assertion:
binary_search.adb:37:50: medium: assertion might fail, cannot prove A (Index) /= I
37 | pragma Assert (for all Index in A'Range => A (Index) /= I);
| ^~~~~~~~~~~~~~
possible fix: precondition of subprogram at binary_search.ads:18 should mention I
18 | function Search (A : Ar; I : Integer) return Opt_Index with
| ^ here
The problem is that GNATprove only knows what the user specified about A
in the precondition, namely that it is sorted in ascending order. Nowhere it is
said that A
does not contain the value I
. Note that adding this
assertion is not compulsory. It simply helps identifying what is needed to
achieve property [AFTER], but it can be removed afterwards.
What is needed here is a loop invariant stating that, if A
contains the
value I
, it must be at an index in the range Left..Right
, so when the
loop exits because Left > Right
(so the loop test becomes false), A
cannot contain the value I
.
One way to express this property is to state that the value of A
at
index Left - 1
is less than I
, while the value of A
at index
Right + 1
is greater than I
. Taking into account the possibility that
there are no such indexes in A
if either Left
or Right
are at the
boundaries of the array, we can express it as follows:
while Left <= Right loop
pragma Loop_Variant (Increases => Left, Decreases => Right);
pragma Loop_Invariant (Left in A'Range and Right in A'Range);
pragma Loop_Invariant (Left = A'First or else A (Left - 1) < I);
pragma Loop_Invariant (Right = A'Last or else I < A (Right + 1));
GNATprove manages to prove these additional loop invariants, but it still cannot prove the assertion after the loop. The reason is both simple and far-reaching. Although the above loop invariant together with the property that the array is sorted imply the property we want to express, it still requires additional work for the prover to reach the same conclusion, which may prevent automatic proof in the allocated time. In that case, it is better to express the equivalent but more explicit property directly, as follows:
while Left <= Right loop
pragma Loop_Variant (Increases => Left, Decreases => Right);
pragma Loop_Invariant (Left in A'Range and Right in A'Range);
pragma Loop_Invariant
(for all Index in A'First .. Left - 1 => A (Index) < I);
pragma Loop_Invariant
(for all Index in A'Range =>
(if Index > Right then I < A (Index)));
GNATprove now proves the assertion after the loop. In general, it is simpler to understand the relationship between the loop invariant and the checks that follow the loop when the loop invariant is directly followed by the exit statement that controls loop termination. In a “for” or “while” loop, this can mean it is easier to place the Loop_Invariant pragmas at the end of the loop body, where they precede the (implicit) exit statement. In such cases, the loop invariant is more likely to resemble the postcondition.
7.7.7. Proving a Loop Invariant After the First Iteration
With the loop invariant given before, GNATprove also proves that the loop
invariant of Search
holds after the first iteration, which corresponds to
property [PRESERVE]. In fact, we have now arrived at a loop invariant which
allows GNATprove to prove all checks for subprogram Search
.
This is not always the case. In general, when the loop invariant is not proved after the first iteration, the problem is that the loop invariant is not precise enough. The only information that GNATprove knows about the value of variables that are modified in the loop, at each loop iteration, is the information provided in the loop invariant. If the loop invariant is missing some crucial information about these variables, which is needed to prove the loop invariant after N iterations, GNATprove won’t be able to prove that the loop invariant holds at each iteration.
In loops that modify variables of composite types (records and arrays), it is usually necessary at this stage to add in the loop invariant some information about those parts of the modified variables which are not modified by the loop, or which are not modified in the first N iterations of the loop. Otherwise, GNATprove assumes that these parts may also be modified, which can prevent it from proving the preservation of the loop invariant. See Loop Invariants for an example where this is needed.
In other cases, it may be necessary to guide the prover with intermediate assertions. A rule of thumb for deciding which properties to assert, and where to assert them, is to try to locate at which program point the prover does not success in proving the property of interest, and to restate other properties that are useful for the proof.
In yet other cases, where the difficulty is related to the size of the loop rather than the complexity of the properties, it may be useful to factor the loop into local subprograms so that the subprograms’ preconditions and postconditions provide the intermediate assertions that are needed to prove the loop invariant.