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 to Idx have been updated in the loop.

  • To prove the postcondition of Update_Rec, one needs to know that only the component A of record R 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:

  1. [INIT] It should be provable in the first iteration of the loop.

  2. [INSIDE] It should allow proving absence of run-time errors and local assertions inside the loop.

  3. [AFTER] It should allow proving absence of run-time errors, local assertions and the subprogram postcondition after the loop.

  4. [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:

  1. [INIT] It is proved in the first iteration (message on line 3).

  2. [INSIDE] It allows proving absence of run-time errors inside the loop (messages on lines 1 and 4).

  3. [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).

  4. [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.