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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package Frame_Condition with
  SPARK_Mode
is
   type Index is range 1 .. 100;
   type Arr is array (Index) of Integer;

   procedure Update_Arr (A : in out Arr; Idx : Index) with
     Post => A(Idx + 1 .. A'Last) = A(Idx + 1 .. A'Last)'Old;

   type Rec is record
      A : Arr;
      X : Integer;
   end record;

   procedure Update_Rec (R : in out Rec) with
     Post => R.X = R.X'Old;

end Frame_Condition;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package body Frame_Condition with
  SPARK_Mode
is
   procedure Update_Arr (A : in out Arr; Idx : Index) is
   begin
      for J in A'First .. Idx loop
         A(J) := Integer(J);
      end loop;
   end Update_Arr;

   procedure Update_Rec (R : in out Rec) is
   begin
      for J in R.A'Range loop
         R.A(J) := Integer(J);
      end loop;
   end Update_Rec;

end 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:

1
2
3
4
frame_condition.ads:8:14: info: postcondition proved
frame_condition.ads:8:14: info: range check proved
frame_condition.ads:8:37: info: range check proved
frame_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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
procedure Preserved_Fields with SPARK_Mode is
   type R is record
      F1 : Integer := 0;
      F2 : Integer := 0;
   end record;

   type R_Array is array (1 .. 100) of R;

   type R_Array_Record is record
      F3 : R_Array;
      F4 : R_Array;
   end record;

   D : R_Array_Record;

begin
   for I in 1 .. 100 loop
      D.F3 (I).F1 := 0;
      pragma Assert (for all J in 1 .. 100 =>
                       D.F3 (J).F2 = D.F3'Loop_Entry (J).F2);
      pragma Assert (D.F4 = D.F4'Loop_Entry);
   end loop;

end 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:

1
2
3
4
5
6
7
preserved_fields.adb:18:19: info: initialization of "D.F3" proved
preserved_fields.adb:19:22: info: assertion proved
preserved_fields.adb:20:24: info: initialization of "D.F3" proved
preserved_fields.adb:20:42: info: initialization of "D.F3" proved
preserved_fields.adb:21:22: info: assertion proved
preserved_fields.adb:21:22: info: initialization of "D.F4" proved
preserved_fields.adb:21:33: info: initialization of "D.F4" 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, and so, 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
procedure Preserved_Components with SPARK_Mode is

   type A is array (1 .. 100) of Natural with Default_Component_Value => 1;

   type A_Matrix is array (1 .. 100, 1 .. 100) of A;

   M : A_Matrix;

begin
   L1: for I in 1 .. 100 loop
      M (I, 1) (1 .. 50) := (others => 0);
      pragma Assert
        (for all K1 in 1 .. 100 =>
           (for all K2 in 1 .. 100 =>
                (for all K3 in 1 .. 100 =>
                     (if K1 > I or else K2 /= 1 or else K3 > 50 then
                             M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
   end loop L1;

   L2: for I in 1 .. 99 loop
      M (I + 1, I) (I .. 100) := (others => 0);
      pragma Assert
        (for all K1 in 1 .. 100 =>
           (for all K2 in 1 .. 100 =>
                (for all K3 in 1 .. 100 =>
                     (if K1 > I + 1 then
                             M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
      pragma Assert
        (for all K1 in 1 .. 100 =>
           (for all K2 in 1 .. 100 =>
                (for all K3 in 1 .. 100 =>
                     (if K3 < K2 then
                             M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3)))));
   end loop L2;

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
preserved_components.adb:11:26: info: initialization of "M" proved
preserved_components.adb:13:10: info: assertion proved
preserved_components.adb:17:30: info: initialization of "M" proved
preserved_components.adb:17:49: info: initialization of "M" proved
preserved_components.adb:21:31: info: initialization of "M" proved
preserved_components.adb:21:31: info: length check proved
preserved_components.adb:21:34: info: length check proved
preserved_components.adb:27:30: info: initialization of "M" proved
preserved_components.adb:27:30: medium: assertion might fail, cannot prove M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3) (e.g. when I = 0 and K1 = 0 and K2 = 0 and K3 = 0 and M = !)
preserved_components.adb:27:49: info: initialization of "M" proved
preserved_components.adb:33:30: info: initialization of "M" proved
preserved_components.adb:33:30: medium: assertion might fail, cannot prove M (K1, K2) (K3) = M'Loop_Entry (K1, K2) (K3) (e.g. when K1 = 0 and K2 = 0 and K3 = 0 and M = !)
preserved_components.adb:33:49: info: initialization of "M" proved

Note

The generation of loop invariants for unmodified components of record variables is available starting with SPARK Pro 17. The generation of loop invariants for unmodified array components for arrays up to the current loop index is available starting with SPARK Pro 18 wavefronts.

7.7.2. 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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
package Linear_Search 
  with SPARK_Mode
is
   type Opt_Index is new Natural;

   subtype Index is Opt_Index range 1 .. Opt_Index'Last - 1;

   No_Index : constant Opt_Index := 0;

   type Ar is array (Index range <>) of Integer;

   function Search (A : Ar; I : Integer) return Opt_Index with
     Post => (if Search'Result in A'Range then A (Search'Result) = I
              else (for all K in A'Range => A (K) /= I));

end 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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package body Linear_Search 
  with SPARK_Mode
is

   function Search (A : Ar; I : Integer) return Opt_Index is
   begin
      for Pos in A'Range loop
         if A (Pos) = I then
            return Pos;
         end if;

         pragma Loop_Invariant (for all K in A'First .. Pos => A (K) /= I);
      end loop;

      return No_Index;
   end Search;

end 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:

1
2
3
4
5
6
7
linear_search.adb:9:20: info: range check proved
linear_search.adb:12:33: info: loop invariant initialization proved
linear_search.adb:12:33: info: loop invariant preservation proved
linear_search.adb:12:67: info: index check proved
linear_search.ads:13:14: info: postcondition proved
linear_search.ads:13:57: info: index check proved
linear_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 2).
  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 3).

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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package Binary_Search
  with SPARK_Mode
is
   type Opt_Index is new Natural;

   subtype Index is Opt_Index range 1 .. Opt_Index'Last - 1;

   No_Index : constant Opt_Index := 0;

   type Ar is array (Index range <>) of Integer;

   function Empty (A : Ar) return Boolean is (A'First > A'Last);

   function Sorted (A : Ar) return Boolean is
      (for all I1 in A'Range =>
         (for all I2 in I1 .. A'Last => A (I1) <= A (I2)));

   function Search (A : Ar; I : Integer) return Opt_Index with
     Pre  => Sorted (A),
     Post => (if Search'Result in A'Range then A (Search'Result) = I
              else (for all Index in A'Range => A (Index) /= I));

end Binary_Search;

The implementation of Binary_Search is given in file binary_search.adb:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
package body Binary_Search
  with SPARK_Mode
is

   function Search (A : Ar; I : Integer) return Opt_Index is
      Left  : Index;
      Right : Index;
      Med   : Index;
   begin
      if Empty (A) then
         return No_Index;
      end if;

      Left  := A'First;
      Right := A'Last;

      if Left = Right and A (Left) = I then
         return Left;
      elsif A (Left) > I or A (Right) < I then
         return No_Index;
      end if;

      while Left <= Right loop
         Med := Left + (Right - Left) / 2;

         if A (Med) < I then
            Left := Med + 1;
         elsif A (Med) > I then
            Right := Med - 1;
         else
            return Med;
         end if;
      end loop;

      return No_Index;
   end Search;

end 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 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.3. 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.4. 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:26:16: medium: array index check might fail (e.g. when A = (2 => 0, others => -1) and A'First = 1 and A'Last = 2 and Med = 3)
binary_search.ads:21:49: medium: postcondition might fail, cannot prove A (Index) /= I (e.g. when A = (0 => 0, 3 => 0, others => -1) and A'First = 1 and A'Last = 3 and I = 0 and Index = 3 and Search'Result = 0)

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_Invariant (Left in A'Range and Right in A'Range);
         
         Med := Left + (Right - Left) / 2;

With this simple loop invariant, GNATprove now reports that the check on lines 27 is now proved. GNATprove computes that the value assigned to Med in the loop is also within the bounds of A.

7.7.5. 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 (e.g. when A = (1 => -1, 3 => 1, others => 0) and A'First = 1 and A'Last = 3 and I = 0 and Index = 2 and Search'Result = 0)

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 loop;
      pragma Assert (for all Index in A'Range => A (Index) /= I);
      
      return No_Index;

GNATprove now succeeds in proving the postcondition, but it fails to prove the assertion:

binary_search.adb:36:50: medium: assertion might fail, cannot prove A (Index) /= I (e.g. when A = (0 => 0, 2 => 0, others => -1) and A'First = 1 and A'Last = 2 and I = 0 and Index = 2)

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_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));
         
         Med := Left + (Right - Left) / 2;

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_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)));
         
         Med := Left + (Right - Left) / 2;

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.6. 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 into local subprograms so that the subprograms’ preconditions and postconditions provide the intermediate assertions that are needed to prove the loop invariant.