7.9.2. Loop Examples

The examples in this section contain loops, and thus require in general that users write suitable Loop Invariants. We start by explaining the need for a loop invariant, and we continue with a description of the most common patterns of loops and their loop invariant. We summarize each pattern in a table of the following form:

Loop Pattern Loop Over Data Structure
Proof Objective Establish property P.
Loop Behavior Loops over the data structure and establishes P.
Loop Invariant Property P is established for the part of the data structure looped over so far.

The examples in this section use the types defined in package Loop_Types:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
with Ada.Containers.Formal_Doubly_Linked_Lists;
with Ada.Containers.Formal_Vectors;

package Loop_Types
  with SPARK_Mode
is
   subtype Index_T is Positive range 1 .. 1000;
   subtype Opt_Index_T is Natural range 0 .. 1000;
   subtype Component_T is Natural;

   type Arr_T is array (Index_T) of Component_T;

   package Vectors is new Ada.Containers.Formal_Vectors (Index_T, Component_T);
   subtype Vec_T is Vectors.Vector;

   package Lists is new Ada.Containers.Formal_Doubly_Linked_Lists (Component_T);
   subtype List_T is Lists.List;

end Loop_Types;

7.9.2.1. The Need for a Loop Invariant

Consider a simple procedure that increments its integer parameter X a number N of times:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
procedure Increment_Loop (X : in out Integer; N : Natural) with
  SPARK_Mode,
  Pre  => X <= Integer'Last - N,
  Post => X = X'Old + N
is
begin
   for I in 1 .. N loop
      X := X + 1;
   end loop;
end Increment_Loop;

The precondition of Increment_Loop ensures that there is no overflow when incrementing X in the loop, and its postcondition states that X has been incremented N times. This contract is a generalization of the contract given for a single increment in Increment. GNATprove does not manage to prove either the absence of overflow or the postcondition of Increment_Loop:

increment_loop.adb:3:29: info: overflow check proved
increment_loop.adb:4:11: medium: postcondition might fail, cannot prove X = X'Old + N (e.g. when N = 1 and X = 1 and X'Old = 1)
increment_loop.adb:4:21: info: overflow check proved
increment_loop.adb:8:14: medium: overflow check might fail (e.g. when X = 2147483647)

As described in How to Write Loop Invariants, this is because variable X is modified in the loop, hence GNATprove knows nothing about it unless it is stated in a loop invariant. If we add such a loop invariant that describes precisely the value of X in each iteration of the loop:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
procedure Increment_Loop_Inv (X : in out Integer; N : Natural) with
  SPARK_Mode,
  Pre  => X <= Integer'Last - N,
  Post => X = X'Old + N
is
begin
   for I in 1 .. N loop
      X := X + 1;
      pragma Loop_Invariant (X = X'Loop_Entry + I);
   end loop;
end Increment_Loop_Inv;

then GNATprove proves both the absence of overflow and the postcondition of Increment_Loop_Inv:

increment_loop_inv.adb:3:29: info: overflow check proved
increment_loop_inv.adb:4:11: info: postcondition proved
increment_loop_inv.adb:4:21: info: overflow check proved
increment_loop_inv.adb:8:14: info: overflow check proved
increment_loop_inv.adb:9:30: info: loop invariant initialization proved
increment_loop_inv.adb:9:30: info: loop invariant preservation proved
increment_loop_inv.adb:9:47: info: overflow check proved

Fortunately, many loops fall into some broad categories for which the loop invariant is known. In the following sections, we describe these common patterns of loops and their loop invariant, which involve in general iterating over the content of a collection (either an array or a container from the Formal Containers Library).

7.9.2.2. Initialization Loops

This kind of loops iterates over a collection to initialize every element of the collection to a given value:

Loop Pattern Separate Initialization of Each Element
Proof Objective Every element of the collection has a specific value.
Loop Behavior Loops over the collection and initializes every element of the collection.
Loop Invariant Every element initialized so far has its specific value.

In the simplest case, every element is assigned the same value. For example, in procedure Init_Arr_Zero below, value zero is assigned to every element of array A:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Loop_Types; use Loop_Types;

procedure Init_Arr_Zero (A : out Arr_T) with
  SPARK_Mode,
  Post => (for all J in A'Range => A(J) = 0)
is
begin
   for J in A'Range loop
      A(J) := 0;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) = 0);
      pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
                       "Part of array up to index J is initialized at this point");
   end loop;
end Init_Arr_Zero;

The loop invariant expresses that all elements up to the current loop index J have the value zero. With this loop invariant, GNATprove is able to prove the postcondition of Init_Arr_Zero, namely that all elements of the array have value zero:

init_arr_zero.adb:3:26: info: initialization of "A" proved
init_arr_zero.adb:5:11: info: postcondition proved
init_arr_zero.adb:5:36: info: initialization of "A" proved
init_arr_zero.adb:10:30: info: loop invariant initialization proved
init_arr_zero.adb:10:30: info: loop invariant preservation proved
init_arr_zero.adb:10:59: info: initialization of "A" proved
init_arr_zero.adb:10:61: info: index check proved

Note

Pragma Annotate is used in Init_Arr_Zero to justify a message issued by flow analysis, about the possible read of uninitialized value A(K) in the loop invariant. Indeed, flow analysis is not currently able to infer that all elements up to the loop index J have been initialized, hence it issues a message that "A" might not be initialized. For more details, see section on Justifying Check Messages.

Consider now a variant of the same initialization loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;

procedure Init_Vec_Zero (V : in out Vec_T) with
  SPARK_Mode,
  Post => (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0)
is
begin
   for J in First_Index (V) .. Last_Index (V) loop
      Replace_Element (V, J, 0);
      pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
      pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) = 0);
   end loop;
end Init_Vec_Zero;

Like before, the loop invariant expresses that all elements up to the current loop index J have the value zero. Another loop invariant is needed here to express that the length of the vector does not change in the loop: as variable V is modified in the loop, GNATprove does not know its length stays the same (for example, calling procedure Append or Delete_Last would change this length) unless the user says so in the loop invariant. This is different from arrays whose length cannot change. With this loop invariant, GNATprove is able to prove the postcondition of Init_Vec_Zero, namely that all elements of the vector have value zero:

init_vec_zero.adb:5:11: info: postcondition proved
init_vec_zero.adb:5:62: info: precondition proved
init_vec_zero.adb:5:74: info: range check proved
init_vec_zero.adb:9:07: info: precondition proved
init_vec_zero.adb:9:27: info: range check proved
init_vec_zero.adb:10:30: info: loop invariant initialization proved
init_vec_zero.adb:10:30: info: loop invariant preservation proved
init_vec_zero.adb:11:30: info: loop invariant initialization proved
init_vec_zero.adb:11:30: info: loop invariant preservation proved
init_vec_zero.adb:11:67: info: precondition proved
init_vec_zero.adb:11:79: info: range check proved

Similarly, consider a variant of the same initialization loop over a list:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Init_List_Zero (L : in out List_T) with
  SPARK_Mode,
  Post => (for all E of L => E = 0)
is
   Cu : Cursor := First (L);
begin
   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
                               Element (Model (L), I) = 0);
      Replace_Element (L, Cu, 0);
      Next (L, Cu);
   end loop;
end Init_List_Zero;

Contrary to arrays and vectors, lists are not indexed. Instead, a cursor can be defined to iterate over the list. The loop invariant expresses that all elements up to the current cursor Cu have the value zero. To access the element stored at a given position in a list, we use the function Model which computes the mathematical sequence of the elements stored in the list. The position of a cursor in this sequence is retrieved using the Positions function. Contrary to the case of vectors, no loop invariant is needed to express that the length of the list does not change in the loop, because the postcondition remains provable here even if the length of the list changes. With this loop invariant, GNATprove is able to prove the postcondition of Init_List_Zero, namely that all elements of the list have value zero:

init_list_zero.adb:6:11: info: postcondition proved
init_list_zero.adb:6:12: info: precondition proved
init_list_zero.adb:10:26: info: initialization of "Cu.Node" proved
init_list_zero.adb:11:30: info: loop invariant initialization proved
init_list_zero.adb:11:30: info: loop invariant preservation proved
init_list_zero.adb:11:49: info: precondition proved
init_list_zero.adb:11:70: info: initialization of "Cu.Node" proved
init_list_zero.adb:12:32: info: precondition proved
init_list_zero.adb:13:07: info: precondition proved
init_list_zero.adb:13:27: info: initialization of "Cu.Node" proved
init_list_zero.adb:14:07: info: precondition proved
init_list_zero.adb:14:16: info: initialization of "Cu.Node" proved

The case of sets and maps is similar to the case of lists.

Note

The parameter of Init_Vec_Zero and Init_List_Zero is an in out parameter. This is because some components of the vector/list parameter are preserved by the initialization procedure (in particular the component corresponding to its length). This is different from Init_Arr_Zero which takes an out parameter, as all components of the array are initialized by the procedure (the bounds of an array are not modifiable, hence considered separately from the parameter mode).

Consider now a case where the value assigned to each element is not the same. For example, in procedure Init_Arr_Index below, each element of array A is assigned the value of its index:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Loop_Types; use Loop_Types;

procedure Init_Arr_Index (A : out Arr_T) with
  SPARK_Mode,
  Post => (for all J in A'Range => A(J) = J)
is
begin
   for J in A'Range loop
      A(J) := J;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) = K);
      pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
                       "Part of array up to index J is initialized at this point");
   end loop;
end Init_Arr_Index;

The loop invariant expresses that all elements up to the current loop index J have the value of their index. With this loop invariant, GNATprove is able to prove the postcondition of Init_Arr_Index, namely that all elements of the array have the value of their index:

init_arr_index.adb:3:27: info: initialization of "A" proved
init_arr_index.adb:5:11: info: postcondition proved
init_arr_index.adb:5:36: info: initialization of "A" proved
init_arr_index.adb:10:30: info: loop invariant initialization proved
init_arr_index.adb:10:30: info: loop invariant preservation proved
init_arr_index.adb:10:59: info: initialization of "A" proved
init_arr_index.adb:10:61: info: index check proved

Similarly, variants of Init_Vec_Zero and Init_List_Zero that assign a different value to each element of the collection would be proved by GNATprove.

7.9.2.3. Mapping Loops

This kind of loops iterates over a collection to map every element of the collection to a new value:

Loop Pattern Separate Modification of Each Element
Proof Objective Every element of the collection has an updated value.
Loop Behavior Loops over the collection and updates every element of the collection.
Loop Invariant Every element updated so far has its specific value.

In the simplest case, every element is assigned a new value based only on its initial value. For example, in procedure Map_Arr_Incr below, every element of array A is incremented by one:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
with Loop_Types; use Loop_Types;

procedure Map_Arr_Incr (A : in out Arr_T) with
  SPARK_Mode,
  Pre  => (for all J in A'Range => A(J) /= Component_T'Last),
  Post => (for all J in A'Range => A(J) = A'Old(J) + 1)
is
begin
   for J in A'Range loop
      A(J) := A(J) + 1;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) = A'Loop_Entry(K) + 1);
      --  The following loop invariant is generated automatically by GNATprove:
      --  pragma Loop_Invariant (for all K in J + 1 .. A'Last => A(K) = A'Loop_Entry(K));
   end loop;
end Map_Arr_Incr;

The loop invariant expresses that all elements up to the current loop index J have been incremented (using Attribute Loop_Entry). With this loop invariant, GNATprove is able to prove the postcondition of Map_Arr_Incr, namely that all elements of the array have been incremented:

map_arr_incr.adb:6:11: info: postcondition proved
map_arr_incr.adb:6:52: info: overflow check proved
map_arr_incr.adb:10:20: info: overflow check proved
map_arr_incr.adb:11:30: info: loop invariant initialization proved
map_arr_incr.adb:11:30: info: loop invariant preservation proved
map_arr_incr.adb:11:61: info: index check proved
map_arr_incr.adb:11:79: info: index check proved
map_arr_incr.adb:11:82: info: overflow check proved

Note that the commented loop invariant expressing that other elements have not been modified is not needed, as it is an example of Automatically Generated Loop Invariants.

Consider now a variant of the same initialization loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
pragma Unevaluated_Use_Of_Old (Allow);
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
use Loop_Types.Vectors.Formal_Model;

procedure Map_Vec_Incr (V : in out Vec_T) with
  SPARK_Mode,
  Pre  => (for all I in 1 .. Last_Index (V) =>
               Element (V, I) /= Component_T'Last),
  Post => Last_Index (V) = Last_Index (V)'Old
  and then (for all I in 1 .. Last_Index (V) =>
                 Element (V, I) = Element (Model (V)'Old, I) + 1)
is
begin
   for J in 1 .. Last_Index (V) loop
      pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
      pragma Loop_Invariant
        (for all I in 1 .. J - 1 =>
           Element (V, I) = Element (Model (V)'Loop_Entry, I) + 1);
      pragma Loop_Invariant
        (for all I in J .. Last_Index (V) =>
           Element (V, I) = Element (Model (V)'Loop_Entry, I));
      Replace_Element (V, J, Element (V, J) + 1);
   end loop;
end Map_Vec_Incr;

Like before, we need an additionnal loop invariant to state that the length of the vector is not modified by the loop. The other two invariants are direct translations of those used for the loop over arrays: the first one expresses that all elements up to the current loop index J have been incremented, and the second one expresses that other elements have not been modified. Note that, as formal vectors are limited, we need to use the Model function of vectors to express the set of elements contained in the vector before the loop (using attributes Loop_Entry and Old). With this loop invariant, GNATprove is able to prove the postcondition of Map_Vec_Incr, namely that all elements of the vector have been incremented:

map_vec_incr.adb:8:16: info: precondition proved
map_vec_incr.adb:8:28: info: range check proved
map_vec_incr.adb:9:11: info: postcondition proved
map_vec_incr.adb:11:18: info: precondition proved
map_vec_incr.adb:11:30: info: range check proved
map_vec_incr.adb:11:35: info: precondition proved
map_vec_incr.adb:11:59: info: range check proved
map_vec_incr.adb:11:62: info: overflow check proved
map_vec_incr.adb:15:30: info: loop invariant initialization proved
map_vec_incr.adb:15:30: info: loop invariant preservation proved
map_vec_incr.adb:17:10: info: loop invariant initialization proved
map_vec_incr.adb:17:10: info: loop invariant preservation proved
map_vec_incr.adb:18:12: info: precondition proved
map_vec_incr.adb:18:24: info: range check proved
map_vec_incr.adb:18:29: info: precondition proved
map_vec_incr.adb:18:60: info: range check proved
map_vec_incr.adb:18:63: info: overflow check proved
map_vec_incr.adb:20:10: info: loop invariant initialization proved
map_vec_incr.adb:20:10: info: loop invariant preservation proved
map_vec_incr.adb:21:12: info: precondition proved
map_vec_incr.adb:21:24: info: range check proved
map_vec_incr.adb:21:29: info: precondition proved
map_vec_incr.adb:21:60: info: range check proved
map_vec_incr.adb:22:07: info: precondition proved
map_vec_incr.adb:22:27: info: range check proved
map_vec_incr.adb:22:30: info: precondition proved
map_vec_incr.adb:22:42: info: range check proved
map_vec_incr.adb:22:45: info: overflow check proved

Similarly, consider a variant of the same initialization loop over a list:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Map_List_Incr (L : in out List_T) with
  SPARK_Mode,
  Pre  => (for all E of L => E /= Component_T'Last),
  Post => Length (L) = Length (L)'Old
  and then (for all I in 1 .. Length (L) =>
                 Element (Model (L), I) = Element (Model (L'Old), I) + 1)
is
   Cu : Cursor := First (L);
begin
   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
      pragma Loop_Invariant
        (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
           Element (Model (L), I) = Element (Model (L'Loop_Entry), I) + 1);
      pragma Loop_Invariant
        (for all I in P.Get (Positions (L), Cu) .. Length (L) =>
           Element (Model (L), I) = Element (Model (L'Loop_Entry), I));
      Replace_Element (L, Cu, Element (L, Cu) + 1);
      Next (L, Cu);
   end loop;
end Map_List_Incr;

Like before, we need to use a cursor to iterate over the list. The loop invariants express that all elements up to the current loop index J have been incremented and that other elements have not been modified. Note that it is necessary to state here that the length of the list is not modified during the loop. It is because the length is used to bound the quantification over the elements of the list both in the invariant and in the postcondition. With this loop invariant, GNATprove is able to prove the postcondition of Map_List_Incr, namely that all elements of the list have been incremented:

map_list_incr.adb:6:12: info: precondition proved
map_list_incr.adb:7:11: info: postcondition proved
map_list_incr.adb:9:18: info: precondition proved
map_list_incr.adb:9:43: info: precondition proved
map_list_incr.adb:9:70: info: overflow check proved
map_list_incr.adb:13:26: info: initialization of "Cu.Node" proved
map_list_incr.adb:14:30: info: loop invariant initialization proved
map_list_incr.adb:14:30: info: loop invariant preservation proved
map_list_incr.adb:16:10: info: loop invariant initialization proved
map_list_incr.adb:16:10: info: loop invariant preservation proved
map_list_incr.adb:16:29: info: precondition proved
map_list_incr.adb:16:50: info: initialization of "Cu.Node" proved
map_list_incr.adb:17:12: info: precondition proved
map_list_incr.adb:17:37: info: precondition proved
map_list_incr.adb:17:71: info: overflow check proved
map_list_incr.adb:19:10: info: loop invariant initialization proved
map_list_incr.adb:19:10: info: loop invariant preservation proved
map_list_incr.adb:19:24: info: precondition proved
map_list_incr.adb:19:45: info: initialization of "Cu.Node" proved
map_list_incr.adb:20:12: info: precondition proved
map_list_incr.adb:20:32: info: range check proved
map_list_incr.adb:20:37: info: precondition proved
map_list_incr.adb:20:68: info: range check proved
map_list_incr.adb:21:07: info: precondition proved
map_list_incr.adb:21:27: info: initialization of "Cu.Node" proved
map_list_incr.adb:21:31: info: precondition proved
map_list_incr.adb:21:43: info: initialization of "Cu.Node" proved
map_list_incr.adb:21:47: info: overflow check proved
map_list_incr.adb:22:07: info: precondition proved
map_list_incr.adb:22:16: info: initialization of "Cu.Node" proved

7.9.2.4. Validation Loops

This kind of loops iterates over a collection to validate that every element of the collection has a valid value. The most common pattern is to exit or return from the loop if an invalid value if encountered:

Loop Pattern Sequence Validation with Early Exit
Proof Objective Determine (flag) if there are any invalid elements in a given collection.
Loop Behavior Loops over the collection and exits/returns if an invalid element is encountered.
Loop Invariant Every element encountered so far is valid.

Consider a procedure Validate_Arr_Zero that checks that all elements of an array A have value zero:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
with Loop_Types; use Loop_Types;

procedure Validate_Arr_Zero (A : Arr_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for all J in A'Range => A(J) = 0)
is
begin
   for J in A'Range loop
      if A(J) /= 0 then
         Success := False;
         return;
      end if;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) = 0);
   end loop;

   Success := True;
end Validate_Arr_Zero;

The loop invariant expresses that all elements up to the current loop index J have value zero. With this loop invariant, GNATprove is able to prove the postcondition of Validate_Arr_Zero, namely that output parameter Success is True if-and-only-if all elements of the array have value zero:

validate_arr_zero.adb:3:41: info: initialization of "Success" proved
validate_arr_zero.adb:5:11: info: initialization of "Success" proved
validate_arr_zero.adb:5:11: info: postcondition proved
validate_arr_zero.adb:13:30: info: loop invariant initialization proved
validate_arr_zero.adb:13:30: info: loop invariant preservation proved
validate_arr_zero.adb:13:61: info: index check proved

Consider now a variant of the same validation loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;

procedure Validate_Vec_Zero (V : Vec_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0)
is
begin
   for J in First_Index (V) .. Last_Index (V) loop
      if Element (V, J) /= 0 then
         Success := False;
         return;
      end if;
      pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) = 0);
   end loop;

   Success := True;
end Validate_Vec_Zero;

Like before, the loop invariant expresses that all elements up to the current loop index J have the value zero. Since variable V is not modified in the loop, no additional loop invariant is needed here for GNATprove to know that its length stays the same (this is different from the case of Init_Vec_Zero seen previously). With this loop invariant, GNATprove is able to prove the postcondition of Validate_Vec_Zero, namely that output parameter Success is True if-and-only-if all elements of the vector have value zero:

validate_vec_zero.adb:3:41: info: initialization of "Success" proved
validate_vec_zero.adb:5:11: info: initialization of "Success" proved
validate_vec_zero.adb:5:11: info: postcondition proved
validate_vec_zero.adb:5:72: info: precondition proved
validate_vec_zero.adb:5:84: info: range check proved
validate_vec_zero.adb:9:10: info: precondition proved
validate_vec_zero.adb:9:22: info: range check proved
validate_vec_zero.adb:13:30: info: loop invariant initialization proved
validate_vec_zero.adb:13:30: info: loop invariant preservation proved
validate_vec_zero.adb:13:67: info: precondition proved
validate_vec_zero.adb:13:79: info: range check proved

Similarly, consider a variant of the same validation loop over a list:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Validate_List_Zero (L : List_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for all E of L => E = 0)
is
   Cu : Cursor := First (L);
begin
   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
                               Element (Model (L), I) = 0);
      if Element (L, Cu) /= 0 then
         Success := False;
         return;
      end if;
      Next (L, Cu);
   end loop;

   Success := True;
end Validate_List_Zero;

Like in the case of Init_List_Zero seen previously, we need to define a cursor here to iterate over the list. The loop invariant expresses that all elements up to the current cursor Cu have the value zero. With this loop invariant, GNATprove is able to prove the postcondition of Validate_List_Zero, namely that output parameter Success is True if-and-only-if all elements of the list have value zero:

validate_list_zero.adb:4:43: info: initialization of "Success" proved
validate_list_zero.adb:6:11: info: initialization of "Success" proved
validate_list_zero.adb:6:11: info: postcondition proved
validate_list_zero.adb:6:22: info: precondition proved
validate_list_zero.adb:10:26: info: initialization of "Cu.Node" proved
validate_list_zero.adb:11:30: info: loop invariant initialization proved
validate_list_zero.adb:11:30: info: loop invariant preservation proved
validate_list_zero.adb:11:49: info: precondition proved
validate_list_zero.adb:11:70: info: initialization of "Cu.Node" proved
validate_list_zero.adb:12:32: info: precondition proved
validate_list_zero.adb:13:10: info: precondition proved
validate_list_zero.adb:13:22: info: initialization of "Cu.Node" proved
validate_list_zero.adb:17:07: info: precondition proved
validate_list_zero.adb:17:16: info: initialization of "Cu.Node" proved

The case of sets and maps is similar to the case of lists.

A variant of the previous validation pattern is to continue validating elements even after an invalid value has been encountered, which allows for example logging all invalid values:

Loop Pattern Sequence Validation that Validates Entire Collection
Proof Objective Determine (flag) if there are any invalid elements in a given collection.
Loop Behavior Loops over the collection. If an invalid element is encountered, flag this, but keep validating (typically logging every invalidity) for the entire collection.
Loop Invariant If invalidity is not flagged, every element encountered so far is valid.

Consider a variant of Validate_Arr_Zero that keeps validating elements of the array after a non-zero element has been encountered:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
with Loop_Types; use Loop_Types;

procedure Validate_Full_Arr_Zero (A : Arr_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for all J in A'Range => A(J) = 0)
is
begin
   Success := True;

   for J in A'Range loop
      if A(J) /= 0 then
         Success := False;
         --  perform some logging here instead of returning
      end if;
      pragma Loop_Invariant (Success = (for all K in A'First .. J => A(K) = 0));
   end loop;
end Validate_Full_Arr_Zero;

The loop invariant has been modified to state that all elements up to the current loop index J have value zero if-and-only-if the output parameter Success is True. This in turn requires to move the assignment of Success before the loop. With this loop invariant, GNATprove is able to prove the postcondition of Validate_Full_Arr_Zero, which is the same as the postcondition of Validate_Arr_Zero, namely that output parameter Success is True if-and-only-if all elements of the array have value zero:

validate_full_arr_zero.adb:3:46: info: initialization of "Success" proved
validate_full_arr_zero.adb:5:11: info: initialization of "Success" proved
validate_full_arr_zero.adb:5:11: info: postcondition proved
validate_full_arr_zero.adb:15:30: info: initialization of "Success" proved
validate_full_arr_zero.adb:15:30: info: loop invariant initialization proved
validate_full_arr_zero.adb:15:30: info: loop invariant preservation proved
validate_full_arr_zero.adb:15:72: info: index check proved

Similarly, variants of Validate_Vec_Zero and Validate_List_Zero that keep validating elements of the collection after a non-zero element has been encountered would be proved by GNATprove.

7.9.2.5. Counting Loops

This kind of loops iterates over a collection to count the number of elements of the collection that satisfy a given criterion:

Loop Pattern Count Elements Satisfying Criterion
Proof Objective Count elements that satisfy a given criterion.
Loop Behavior Loops over the collection. Increments a counter each time the value of an element satisfies the criterion.
Loop Invariant The value of the counter is either 0 when no element encountered so far satisfies the criterion, or a positive number bounded by the current iteration of the loop otherwise.

Consider a procedure Count_Arr_Zero that counts elements with value zero in array A:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
with Loop_Types; use Loop_Types;

procedure Count_Arr_Zero (A : Arr_T; Counter : out Natural) with
  SPARK_Mode,
  Post => (Counter in 0 .. A'Length) and then
          ((Counter = 0) = (for all K in A'Range => A(K) /= 0))
is
begin
   Counter := 0;

   for J in A'Range loop
      if A(J) = 0 then
         Counter := Counter + 1;
      end if;
      pragma Loop_Invariant (Counter in 0 .. J);
      pragma Loop_Invariant ((Counter = 0) = (for all K in A'First .. J => A(K) /= 0));
   end loop;
end Count_Arr_Zero;

The loop invariant expresses that the value of Counter is a natural number bounded by the current loop index J, and that Counter is equal to zero exactly when all elements up to the current loop index have a non-zero value. With this loop invariant, GNATprove is able to prove the postcondition of Count_Arr_Zero, namely that output parameter Counter is a natural number bounded by the length of the array A, and that Counter is equal to zero exactly when all elements in A have a non-zero value:

count_arr_zero.adb:3:38: info: initialization of "Counter" proved
count_arr_zero.adb:5:11: info: postcondition proved
count_arr_zero.adb:5:12: info: initialization of "Counter" proved
count_arr_zero.adb:6:13: info: initialization of "Counter" proved
count_arr_zero.adb:13:21: info: initialization of "Counter" proved
count_arr_zero.adb:13:29: info: overflow check proved
count_arr_zero.adb:15:30: info: initialization of "Counter" proved
count_arr_zero.adb:15:30: info: loop invariant initialization proved
count_arr_zero.adb:15:30: info: loop invariant preservation proved
count_arr_zero.adb:16:30: info: loop invariant initialization proved
count_arr_zero.adb:16:30: info: loop invariant preservation proved
count_arr_zero.adb:16:31: info: initialization of "Counter" proved
count_arr_zero.adb:16:78: info: index check proved

Consider now a variant of the same counting loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;

procedure Count_Vec_Zero (V : Vec_T; Counter : out Natural) with
  SPARK_Mode,
  Post => (Counter in 0 .. Natural (Length (V))) and then
          ((Counter = 0) = (for all K in First_Index (V) .. Last_Index (V) => Element (V, K) /= 0))
is
begin
   Counter := 0;

   for J in First_Index (V) .. Last_Index (V) loop
      if Element (V, J) = 0 then
         Counter := Counter + 1;
      end if;
      pragma Loop_Invariant (Counter in 0 .. J);
      pragma Loop_Invariant ((Counter = 0) = (for all K in First_Index (V) .. J => Element (V, K) /= 0));
   end loop;
end Count_Vec_Zero;

Like before, the loop invariant expresses that the value of Counter is a natural number bounded by the current loop index J, and that Counter is equal to zero exactly when all elements up to the current loop index have a non-zero value. With this loop invariant, GNATprove is able to prove the postcondition of Count_Vec_Zero, namely that output parameter Counter is a natural number bounded by the length of the vector V, and that Counter is equal to zero exactly when all elements in V have a non-zero value:

count_vec_zero.adb:3:38: info: initialization of "Counter" proved
count_vec_zero.adb:5:11: info: postcondition proved
count_vec_zero.adb:5:12: info: initialization of "Counter" proved
count_vec_zero.adb:6:13: info: initialization of "Counter" proved
count_vec_zero.adb:6:79: info: precondition proved
count_vec_zero.adb:6:91: info: range check proved
count_vec_zero.adb:12:10: info: precondition proved
count_vec_zero.adb:12:22: info: range check proved
count_vec_zero.adb:13:21: info: initialization of "Counter" proved
count_vec_zero.adb:13:29: info: overflow check proved
count_vec_zero.adb:15:30: info: initialization of "Counter" proved
count_vec_zero.adb:15:30: info: loop invariant initialization proved
count_vec_zero.adb:15:30: info: loop invariant preservation proved
count_vec_zero.adb:16:30: info: loop invariant initialization proved
count_vec_zero.adb:16:30: info: loop invariant preservation proved
count_vec_zero.adb:16:31: info: initialization of "Counter" proved
count_vec_zero.adb:16:84: info: precondition proved
count_vec_zero.adb:16:96: info: range check proved

7.9.2.6. Search Loops

This kind of loops iterates over a collection to search an element of the collection that meets a given search criterion:

Loop Pattern Search with Early Exit
Proof Objective Find an element or position that meets a search criterion.
Loop Behavior Loops over the collection. Exits when an element that meets the search criterion is found.
Loop Invariant Every element encountered so far does not meet the search criterion.

Consider a procedure Search_Arr_Zero that searches an element with value zero in array A:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
with Loop_Types; use Loop_Types;

procedure Search_Arr_Zero (A : Arr_T; Pos : out Opt_Index_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for some J in A'Range => A(J) = 0) and then
          (if Success then A (Pos) = 0)
is
begin
   for J in A'Range loop
      if A(J) = 0 then
         Success := True;
         Pos := J;
         return;
      end if;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) /= 0);
   end loop;

   Success := False;
   Pos := 0;
end Search_Arr_Zero;

The loop invariant expresses that all elements up to the current loop index J have a non-zero value. With this loop invariant, GNATprove is able to prove the postcondition of Search_Arr_Zero, namely that output parameter Success is True if-and-only-if there is an element of the array that has value zero, and that Pos is the index of such an element:

search_arr_zero.adb:3:39: info: initialization of "Pos" proved
search_arr_zero.adb:3:62: info: initialization of "Success" proved
search_arr_zero.adb:5:11: info: initialization of "Success" proved
search_arr_zero.adb:5:11: info: postcondition proved
search_arr_zero.adb:6:15: info: initialization of "Success" proved
search_arr_zero.adb:6:31: info: index check proved
search_arr_zero.adb:6:31: info: initialization of "Pos" proved
search_arr_zero.adb:15:30: info: loop invariant initialization proved
search_arr_zero.adb:15:30: info: loop invariant preservation proved
search_arr_zero.adb:15:61: info: index check proved

Consider now a variant of the same search loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;

procedure Search_Vec_Zero (V : Vec_T; Pos : out Opt_Index_T; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for some J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0) and then
          (if Success then Element (V, Pos) = 0)
is
begin
   for J in First_Index (V) .. Last_Index (V) loop
      if Element (V, J) = 0 then
         Success := True;
         Pos := J;
         return;
      end if;
      pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) /= 0);
   end loop;

   Success := False;
   Pos := 0;
end Search_Vec_Zero;

Like before, the loop invariant expresses that all elements up to the current loop index J have a non-zero value. With this loop invariant, GNATprove is able to prove the postcondition of Search_Vec_Zero, namely that output parameter Success is True if-and-only-if there is an element of the vector that has value zero, and that Pos is the index of such an element:

search_vec_zero.adb:3:39: info: initialization of "Pos" proved
search_vec_zero.adb:3:62: info: initialization of "Success" proved
search_vec_zero.adb:5:11: info: initialization of "Success" proved
search_vec_zero.adb:5:11: info: postcondition proved
search_vec_zero.adb:5:73: info: precondition proved
search_vec_zero.adb:5:85: info: range check proved
search_vec_zero.adb:6:15: info: initialization of "Success" proved
search_vec_zero.adb:6:28: info: precondition proved
search_vec_zero.adb:6:40: info: initialization of "Pos" proved
search_vec_zero.adb:6:40: info: range check proved
search_vec_zero.adb:10:10: info: precondition proved
search_vec_zero.adb:10:22: info: range check proved
search_vec_zero.adb:12:17: info: range check proved
search_vec_zero.adb:15:30: info: loop invariant initialization proved
search_vec_zero.adb:15:30: info: loop invariant preservation proved
search_vec_zero.adb:15:67: info: precondition proved
search_vec_zero.adb:15:79: info: range check proved

Similarly, consider a variant of the same search loop over a list:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Search_List_Zero (L : List_T; Pos : out Cursor; Success : out Boolean) with
  SPARK_Mode,
  Post => Success = (for some E of L => E = 0) and then
          (if Success then Element (L, Pos) = 0)
is
   Cu : Cursor := First (L);
begin
   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
                               Element (Model (L), I) /= 0);
      if Element (L, Cu) = 0 then
         Success := True;
         Pos := Cu;
         return;
      end if;
      Next (L, Cu);
   end loop;

   Success := False;
   Pos := No_Element;
end Search_List_Zero;

The loop invariant expresses that all elements up to the current cursor Cu have a non-zero value. With this loop invariant, GNATprove is able to prove the postcondition of Search_List_Zero, namely that output parameter Success is True if-and-only-if there is an element of the list that has value zero, and that Pos is the cursor of such an element:

search_list_zero.adb:4:41: info: initialization of "Pos.Node" proved
search_list_zero.adb:4:59: info: initialization of "Success" proved
search_list_zero.adb:6:11: info: initialization of "Success" proved
search_list_zero.adb:6:11: info: postcondition proved
search_list_zero.adb:6:22: info: precondition proved
search_list_zero.adb:7:15: info: initialization of "Success" proved
search_list_zero.adb:7:28: info: precondition proved
search_list_zero.adb:7:40: info: initialization of "Pos.Node" proved
search_list_zero.adb:11:26: info: initialization of "Cu.Node" proved
search_list_zero.adb:12:30: info: loop invariant initialization proved
search_list_zero.adb:12:30: info: loop invariant preservation proved
search_list_zero.adb:12:49: info: precondition proved
search_list_zero.adb:12:70: info: initialization of "Cu.Node" proved
search_list_zero.adb:13:32: info: precondition proved
search_list_zero.adb:14:10: info: precondition proved
search_list_zero.adb:14:22: info: initialization of "Cu.Node" proved
search_list_zero.adb:16:17: info: initialization of "Cu.Node" proved
search_list_zero.adb:19:07: info: precondition proved
search_list_zero.adb:19:16: info: initialization of "Cu.Node" proved

The case of sets and maps is similar to the case of lists. For more complex examples of search loops, see the SPARK Tutorial as well as the section on How to Write Loop Invariants.

7.9.2.7. Maximize Loops

This kind of loops iterates over a collection to search an element of the collection that maximizes a given optimality criterion:

Loop Pattern Search Optimum to Criterion
Proof Objective Find an element or position that maximizes an optimality criterion.
Loop Behavior Loops over the collection. Records maximum value of criterion so far and possibly index that maximizes this criterion.
Loop Invariant Exactly one element encountered so far corresponds to the recorded maximum over other elements encountered so far.

Consider a procedure Search_Arr_Max that searches an element maximum value in array A:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
with Loop_Types; use Loop_Types;

procedure Search_Arr_Max (A : Arr_T; Pos : out Index_T; Max : out Component_T) with
  SPARK_Mode,
  Post => (for all J in A'Range => A(J) <= Max) and then
          (for some J in A'Range => A(J) = Max) and then
          A(Pos) = Max
is
begin
   Max := 0;
   Pos := A'First;

   for J in A'Range loop
      if A(J) > Max then
         Max := A(J);
         Pos := J;
      end if;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) <= Max);
      pragma Loop_Invariant (for some K in A'First .. J => A(K) = Max);
      pragma Loop_Invariant (A(Pos) = Max);
   end loop;
end Search_Arr_Max;

The loop invariant expresses that all elements up to the current loop index J have a value less than Max, and that Max is the value of one of these elements. The last loop invariant gives in fact this element, it is A(Pos), but this part of the loop invariant may not be present if the position Pos for the optimum is not recorded. With this loop invariant, GNATprove is able to prove the postcondition of Search_Arr_Max, namely that output parameter Max is the maximum of the elements in the array, and that Pos is the index of such an element:

search_arr_max.adb:3:38: info: initialization of "Pos" proved
search_arr_max.adb:3:57: info: initialization of "Max" proved
search_arr_max.adb:5:11: info: postcondition proved
search_arr_max.adb:5:44: info: initialization of "Max" proved
search_arr_max.adb:6:44: info: initialization of "Max" proved
search_arr_max.adb:7:13: info: initialization of "Pos" proved
search_arr_max.adb:7:20: info: initialization of "Max" proved
search_arr_max.adb:14:17: info: initialization of "Max" proved
search_arr_max.adb:18:30: info: loop invariant initialization proved
search_arr_max.adb:18:30: info: loop invariant preservation proved
search_arr_max.adb:18:61: info: index check proved
search_arr_max.adb:18:67: info: initialization of "Max" proved
search_arr_max.adb:19:30: info: loop invariant initialization proved
search_arr_max.adb:19:30: info: loop invariant preservation proved
search_arr_max.adb:19:62: info: index check proved
search_arr_max.adb:19:67: info: initialization of "Max" proved
search_arr_max.adb:20:30: info: loop invariant initialization proved
search_arr_max.adb:20:30: info: loop invariant preservation proved
search_arr_max.adb:20:32: info: initialization of "Pos" proved
search_arr_max.adb:20:39: info: initialization of "Max" proved

Consider now a variant of the same search loop over a vector:

 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
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;

procedure Search_Vec_Max (V : Vec_T; Pos : out Index_T; Max : out Component_T) with
  SPARK_Mode,
  Pre  => not Is_Empty (V),
  Post => (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) <= Max) and then
          (for some J in First_Index (V) .. Last_Index (V) => Element (V, J) = Max) and then
          Pos in First_Index (V) .. Last_Index (V) and then
          Element (V, Pos) = Max
is
begin
   Max := 0;
   Pos := First_Index (V);

   for J in First_Index (V) .. Last_Index (V) loop
      if Element (V, J) > Max then
         Max := Element (V, J);
         Pos := J;
      end if;
      pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) <= Max);
      pragma Loop_Invariant (for some K in First_Index (V) .. J => Element (V, K) = Max);
      pragma Loop_Invariant (Pos in First_Index (V) .. J);
      pragma Loop_Invariant (Element (V, Pos) = Max);
   end loop;
end Search_Vec_Max;

Like before, the loop invariant expresses that all elements up to the current loop index J have a value less than Max, and that Max is the value of one of these elements, most precisely the value of Element (V, Pos) if the position Pos for the optimum is recorded. An additional loop invariant is needed here compared to the case of arrays to state that Pos remains within the bounds of the vector. With this loop invariant, GNATprove is able to prove the postcondition of Search_Vec_Max, namely that output parameter Max is the maximum of the elements in the vector, and that Pos is the index of such an element:

search_vec_max.adb:3:38: info: initialization of "Pos" proved
search_vec_max.adb:3:57: info: initialization of "Max" proved
search_vec_max.adb:6:11: info: postcondition proved
search_vec_max.adb:6:62: info: precondition proved
search_vec_max.adb:6:74: info: range check proved
search_vec_max.adb:6:80: info: initialization of "Max" proved
search_vec_max.adb:7:63: info: precondition proved
search_vec_max.adb:7:75: info: range check proved
search_vec_max.adb:7:80: info: initialization of "Max" proved
search_vec_max.adb:8:11: info: initialization of "Pos" proved
search_vec_max.adb:9:11: info: precondition proved
search_vec_max.adb:9:23: info: initialization of "Pos" proved
search_vec_max.adb:9:30: info: initialization of "Max" proved
search_vec_max.adb:16:10: info: precondition proved
search_vec_max.adb:16:22: info: range check proved
search_vec_max.adb:16:27: info: initialization of "Max" proved
search_vec_max.adb:17:17: info: precondition proved
search_vec_max.adb:17:29: info: range check proved
search_vec_max.adb:18:17: info: range check proved
search_vec_max.adb:20:30: info: loop invariant initialization proved
search_vec_max.adb:20:30: info: loop invariant preservation proved
search_vec_max.adb:20:67: info: precondition proved
search_vec_max.adb:20:79: info: range check proved
search_vec_max.adb:20:85: info: initialization of "Max" proved
search_vec_max.adb:21:30: info: loop invariant initialization proved
search_vec_max.adb:21:30: info: loop invariant preservation proved
search_vec_max.adb:21:68: info: precondition proved
search_vec_max.adb:21:80: info: range check proved
search_vec_max.adb:21:85: info: initialization of "Max" proved
search_vec_max.adb:22:30: info: initialization of "Pos" proved
search_vec_max.adb:22:30: info: loop invariant initialization proved
search_vec_max.adb:22:30: info: loop invariant preservation proved
search_vec_max.adb:23:30: info: loop invariant initialization proved
search_vec_max.adb:23:30: info: loop invariant preservation proved
search_vec_max.adb:23:30: info: precondition proved
search_vec_max.adb:23:42: info: initialization of "Pos" proved
search_vec_max.adb:23:49: info: initialization of "Max" proved

Similarly, consider a variant of the same search loop over a list:

 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
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Search_List_Max (L : List_T; Pos : out Cursor; Max : out Component_T) with
  SPARK_Mode,
  Pre  => not Is_Empty (L),
  Post => (for all E of L => E <= Max) and then
          (for some E of L => E = Max) and then
          Has_Element (L, Pos) and then
          Element (L, Pos) = Max
is
   Cu : Cursor := First (L);
begin
   Max := 0;
   Pos := Cu;

   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
                               Element (Model (L), I) <= Max);
      pragma Loop_Invariant (Has_Element (L, Pos));
      pragma Loop_Invariant (Max = 0 or else Element (L, Pos) = Max);

      if Element (L, Cu) > Max then
         Max := Element (L, Cu);
         Pos := Cu;
      end if;
      Next (L, Cu);
   end loop;
end Search_List_Max;

The loop invariant expresses that all elements up to the current cursor Cu have a value less than Max, and that Max is the value of one of these elements, most precisely the value of Element (L, Pos) if the cursor Pos for the optimum is recorded. Like for vectors, an additional loop invariant is needed here compared to the case of arrays to state that cursor Pos is a valid cursor of the list. A minor difference is that a loop invariant now starts with Max = 0 or else .. because the loop invariant is stated at the start of the loop (for convenience with the use of First_To_Previous) which requires this modification. With this loop invariant, GNATprove is able to prove the postcondition of Search_List_Max, namely that output parameter Max is the maximum of the elements in the list, and that Pos is the cursor of such an element:

search_list_max.adb:4:40: info: initialization of "Pos.Node" proved
search_list_max.adb:4:58: info: initialization of "Max" proved
search_list_max.adb:7:11: info: postcondition proved
search_list_max.adb:7:12: info: precondition proved
search_list_max.adb:7:35: info: initialization of "Max" proved
search_list_max.adb:8:12: info: precondition proved
search_list_max.adb:8:35: info: initialization of "Max" proved
search_list_max.adb:9:27: info: initialization of "Pos.Node" proved
search_list_max.adb:10:11: info: precondition proved
search_list_max.adb:10:23: info: initialization of "Pos.Node" proved
search_list_max.adb:10:30: info: initialization of "Max" proved
search_list_max.adb:15:11: info: initialization of "Cu.Node" proved
search_list_max.adb:17:26: info: initialization of "Cu.Node" proved
search_list_max.adb:18:30: info: loop invariant initialization proved
search_list_max.adb:18:30: info: loop invariant preservation proved
search_list_max.adb:18:49: info: precondition proved
search_list_max.adb:18:70: info: initialization of "Cu.Node" proved
search_list_max.adb:19:32: info: precondition proved
search_list_max.adb:19:58: info: initialization of "Max" proved
search_list_max.adb:20:30: info: loop invariant initialization proved
search_list_max.adb:20:30: info: loop invariant preservation proved
search_list_max.adb:20:46: info: initialization of "Pos.Node" proved
search_list_max.adb:21:30: info: initialization of "Max" proved
search_list_max.adb:21:30: info: loop invariant initialization proved
search_list_max.adb:21:30: info: loop invariant preservation proved
search_list_max.adb:21:46: info: precondition proved
search_list_max.adb:21:58: info: initialization of "Pos.Node" proved
search_list_max.adb:23:10: info: precondition proved
search_list_max.adb:23:22: info: initialization of "Cu.Node" proved
search_list_max.adb:23:28: info: initialization of "Max" proved
search_list_max.adb:24:17: info: precondition proved
search_list_max.adb:24:29: info: initialization of "Cu.Node" proved
search_list_max.adb:25:17: info: initialization of "Cu.Node" proved
search_list_max.adb:27:07: info: precondition proved
search_list_max.adb:27:16: info: initialization of "Cu.Node" proved

The case of sets and maps is similar to the case of lists. For more complex examples of search loops, see the SPARK Tutorial as well as the section on How to Write Loop Invariants.

7.9.2.8. Update Loops

This kind of loops iterates over a collection to update individual elements based either on their value or on their position. The first pattern we consider is the one that updates elements based on their value:

Loop Pattern Modification of Elements Based on Value
Proof Objective Elements of the collection are updated based on their value.
Loop Behavior Loops over a collection and assigns the elements whose value satisfies a given modification criterion.
Loop Invariant Every element encountered so far has been assigned according to its value.

Consider a procedure Update_Arr_Zero that sets to zero all elements in array A that have a value smaller than a given Threshold:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with Loop_Types; use Loop_Types;

procedure Update_Arr_Zero (A : in out Arr_T; Threshold : Component_T) with
  SPARK_Mode,
  Post => (for all J in A'Range => A(J) = (if A'Old(J) <= Threshold then 0 else A'Old(J)))
is
begin
   for J in A'Range loop
      if A(J) <= Threshold then
         A(J) := 0;
      end if;
      pragma Loop_Invariant (for all K in A'First .. J => A(K) = (if A'Loop_Entry(K) <= Threshold then 0 else A'Loop_Entry(K)));
      --  The following loop invariant is generated automatically by GNATprove:
      --  pragma Loop_Invariant (for all K in J + 1 .. A'Last => A(K) = A'Loop_Entry(K));
   end loop;
end Update_Arr_Zero;

The loop invariant expresses that all elements up to the current loop index J have been zeroed out if initially smaller than Threshold (using Attribute Loop_Entry). With this loop invariant, GNATprove is able to prove the postcondition of Update_Arr_Zero, namely that all elements initially smaller than Threshold have been zeroed out, and that other elements have not been modified:

update_arr_zero.adb:5:11: info: postcondition proved
update_arr_zero.adb:12:30: info: loop invariant initialization proved
update_arr_zero.adb:12:30: info: loop invariant preservation proved
update_arr_zero.adb:12:61: info: index check proved
update_arr_zero.adb:12:83: info: index check proved
update_arr_zero.adb:12:124: info: index check proved

Note that the commented loop invariant expressing that other elements have not been modified is not needed, as it is an example of Automatically Generated Loop Invariants.

Consider now a variant of the same update loop over a vector:

 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
pragma Unevaluated_Use_Of_Old (Allow);
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
use Loop_Types.Vectors.Formal_Model;

procedure Update_Vec_Zero (V : in out Vec_T; Threshold : Component_T) with
  SPARK_Mode,
  Post => Last_Index (V) = Last_Index (V)'Old
  and (for all I in 1 .. Last_Index (V) =>
            Element (V, I) =
             (if Element (Model (V)'Old, I) <= Threshold then 0
              else Element (Model (V)'Old, I)))
is
begin
   for J in First_Index (V) .. Last_Index (V) loop
      pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
      pragma Loop_Invariant
        (for all I in 1 .. J - 1 =>
             Element (V, I) =
              (if Element (Model (V)'Loop_Entry, I) <= Threshold then 0
               else Element (Model (V)'Loop_Entry, I)));
      pragma Loop_Invariant
        (for all I in J .. Last_Index (V) =>
             Element (V, I) = Element (Model (V)'Loop_Entry, I));
      if Element (V, J) <= Threshold then
         Replace_Element (V, J, 0);
      end if;
   end loop;
end Update_Vec_Zero;

Like for Map_Vec_Incr, we need to use the Model function over arrays to access elements of the vector before the loop as the vector type is limited. The loop invariant expresses that all elements up to the current loop index J have been zeroed out if initially smaller than Threshold, that elements that follow the current loop index have not been modified, and that the length of V is not modified (like in Init_Vec_Zero). With this loop invariant, GNATprove is able to prove the postcondition of Update_Vec_Zero:

update_vec_zero.adb:7:11: info: postcondition proved
update_vec_zero.adb:9:13: info: precondition proved
update_vec_zero.adb:9:25: info: range check proved
update_vec_zero.adb:10:18: info: precondition proved
update_vec_zero.adb:10:42: info: range check proved
update_vec_zero.adb:11:20: info: precondition proved
update_vec_zero.adb:11:44: info: range check proved
update_vec_zero.adb:15:30: info: loop invariant initialization proved
update_vec_zero.adb:15:30: info: loop invariant preservation proved
update_vec_zero.adb:17:10: info: loop invariant initialization proved
update_vec_zero.adb:17:10: info: loop invariant preservation proved
update_vec_zero.adb:17:30: info: overflow check proved
update_vec_zero.adb:18:14: info: precondition proved
update_vec_zero.adb:18:26: info: range check proved
update_vec_zero.adb:19:19: info: precondition proved
update_vec_zero.adb:19:50: info: range check proved
update_vec_zero.adb:20:21: info: precondition proved
update_vec_zero.adb:20:52: info: range check proved
update_vec_zero.adb:22:10: info: loop invariant initialization proved
update_vec_zero.adb:22:10: info: loop invariant preservation proved
update_vec_zero.adb:23:14: info: precondition proved
update_vec_zero.adb:23:26: info: range check proved
update_vec_zero.adb:23:31: info: precondition proved
update_vec_zero.adb:23:62: info: range check proved
update_vec_zero.adb:24:10: info: precondition proved
update_vec_zero.adb:24:22: info: range check proved
update_vec_zero.adb:25:10: info: precondition proved
update_vec_zero.adb:25:30: info: range check proved

Similarly, consider a variant of the same update loop over a list:

 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
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Update_List_Zero (L : in out List_T; Threshold : Component_T) with
  SPARK_Mode,
  Post => Length (L) = Length (L)'Old
  and (for all I in 1 .. Length (L) =>
            Element (Model (L), I) =
             (if Element (Model (L'Old), I) <= Threshold then 0
              else Element (Model (L'Old), I)))
is
   Cu : Cursor := First (L);
begin
   while Has_Element (L, Cu) loop
      pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
      pragma Loop_Invariant
        (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
            Element (Model (L), I) =
             (if Element (Model (L'Loop_Entry), I) <= Threshold then 0
              else Element (Model (L'Loop_Entry), I)));
      pragma Loop_Invariant
        (for all I in P.Get (Positions (L), Cu) .. Length (L) =>
            Element (Model (L), I) = Element (Model (L'Loop_Entry), I));
      if Element (L, Cu) <= Threshold then
         Replace_Element (L, Cu, 0);
      end if;
      Next (L, Cu);
   end loop;
end Update_List_Zero;

The loop invariant expresses that all elements up to the current cursor Cu have been zeroed out if initially smaller than Threshold (using function Model to access the element stored at a given position in the list and function Positions to query the position of the current cursor), and that elements that follow the current loop index have not been modified. Note that it is necessary to state here that the length of the list is not modified during the loop. It is because the length is used to bound the quantification over the elements of the list both in the invariant and in the postcondition.

With this loop invariant, GNATprove is able to prove the postcondition of Update_List_Zero, namely that all elements initially smaller than Threshold have been zeroed out, and that other elements have not been modified:

update_list_zero.adb:6:11: info: postcondition proved
update_list_zero.adb:8:13: info: precondition proved
update_list_zero.adb:9:18: info: precondition proved
update_list_zero.adb:10:20: info: precondition proved
update_list_zero.adb:14:26: info: initialization of "Cu.Node" proved
update_list_zero.adb:15:30: info: loop invariant initialization proved
update_list_zero.adb:15:30: info: loop invariant preservation proved
update_list_zero.adb:17:10: info: loop invariant initialization proved
update_list_zero.adb:17:10: info: loop invariant preservation proved
update_list_zero.adb:17:29: info: precondition proved
update_list_zero.adb:17:50: info: initialization of "Cu.Node" proved
update_list_zero.adb:18:13: info: precondition proved
update_list_zero.adb:19:18: info: precondition proved
update_list_zero.adb:20:20: info: precondition proved
update_list_zero.adb:22:10: info: loop invariant initialization proved
update_list_zero.adb:22:10: info: loop invariant preservation proved
update_list_zero.adb:22:24: info: precondition proved
update_list_zero.adb:22:45: info: initialization of "Cu.Node" proved
update_list_zero.adb:23:13: info: precondition proved
update_list_zero.adb:23:33: info: range check proved
update_list_zero.adb:23:38: info: precondition proved
update_list_zero.adb:23:69: info: range check proved
update_list_zero.adb:24:10: info: precondition proved
update_list_zero.adb:24:22: info: initialization of "Cu.Node" proved
update_list_zero.adb:25:10: info: precondition proved
update_list_zero.adb:25:30: info: initialization of "Cu.Node" proved
update_list_zero.adb:27:07: info: precondition proved
update_list_zero.adb:27:16: info: initialization of "Cu.Node" proved

The case of sets and maps is similar to the case of lists.

The second pattern of update loops that we consider now is the one that updates elements based on their position:

Loop Pattern Modification of Elements Based on Position
Proof Objective Elements of the collection are updated based on their position.
Loop Behavior Loops over a collection and assigns the elements whose position satisfies a given modification criterion.
Loop Invariant Every element encountered so far has been assigned according to its position.

Consider a procedure Update_Range_Arr_Zero that sets to zero all elements in array A between indexes First and Last:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
with Loop_Types; use Loop_Types;

procedure Update_Range_Arr_Zero (A : in out Arr_T; First, Last : Index_T) with
  SPARK_Mode,
  Post => A = A'Old'Update (First .. Last => 0)
is
begin
   for J in First .. Last loop
      A(J) := 0;
      pragma Loop_Invariant (A = A'Loop_Entry'Update (First .. J => 0));
   end loop;
end Update_Range_Arr_Zero;

The loop invariant expresses that all elements between First and the current loop index J have been zeroed out, and that other elements have not been modified (using a combination of Attribute Loop_Entry and Attribute Update to express this concisely). With this loop invariant, GNATprove is able to prove the postcondition of Update_Range_Arr_Zero, namely that all elements between First and Last have been zeroed out, and that other elements have not been modified:

update_range_arr_zero.adb:5:11: info: postcondition proved
update_range_arr_zero.adb:10:30: info: loop invariant initialization proved
update_range_arr_zero.adb:10:30: info: loop invariant preservation proved
update_range_arr_zero.adb:10:64: info: range check proved

Consider now a variant of the same update loop over a vector:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
pragma Unevaluated_Use_Of_Old (Allow);
with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
use Loop_Types.Vectors.Formal_Model;

procedure Update_Range_Vec_Zero (V : in out Vec_T; First, Last : Index_T) with
  SPARK_Mode,
  Pre  => Last <= Last_Index (V),
  Post => (for all J in 1 .. Last_Index (V) =>
               (if J in First .. Last then Element (V, J) = 0
                else Element (V, J) = Element (Model (V)'Old, J)))
is
begin
   for J in First .. Last loop
      Replace_Element (V, J, 0);
      pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
      pragma Loop_Invariant
        (for all I in 1 .. Last_Index (V) =>
               (if I in First .. J then Element (V, I) = 0
                else Element (V, I) = Element (Model (V)'Loop_Entry, I)));
   end loop;
end Update_Range_Vec_Zero;

Like for Map_Vec_Incr, we need to use the Model function over arrays to access elements of the vector before the loop as the vector type is limited. The loop invariant expresses that all elements between First and current loop index J have been zeroed, and that other elements have not been modified. With this loop invariant, GNATprove is able to prove the postcondition of Update_Range_Vec_Zero:

update_range_vec_zero.adb:8:11: info: postcondition proved
update_range_vec_zero.adb:9:44: info: precondition proved
update_range_vec_zero.adb:9:56: info: range check proved
update_range_vec_zero.adb:10:22: info: precondition proved
update_range_vec_zero.adb:10:34: info: range check proved
update_range_vec_zero.adb:10:39: info: precondition proved
update_range_vec_zero.adb:10:63: info: range check proved
update_range_vec_zero.adb:14:07: info: precondition proved
update_range_vec_zero.adb:15:30: info: loop invariant initialization proved
update_range_vec_zero.adb:15:30: info: loop invariant preservation proved
update_range_vec_zero.adb:17:10: info: loop invariant initialization proved
update_range_vec_zero.adb:17:10: info: loop invariant preservation proved
update_range_vec_zero.adb:18:41: info: precondition proved
update_range_vec_zero.adb:18:53: info: range check proved
update_range_vec_zero.adb:19:22: info: precondition proved
update_range_vec_zero.adb:19:34: info: range check proved
update_range_vec_zero.adb:19:39: info: precondition proved
update_range_vec_zero.adb:19:70: info: range check proved

Similarly, consider a variant of the same update loop over a list:

 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
with Loop_Types; use Loop_Types; use Loop_Types.Lists;
with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;

procedure Update_Range_List_Zero (L : in out List_T; First, Last : Cursor) with
  SPARK_Mode,
  Pre  => Has_Element (L, First) and then Has_Element (L, Last)
  and then P.Get (Positions (L), First) <= P.Get (Positions (L), Last),
  Post => Length (L) = Length (L)'Old
  and Positions (L) = Positions (L)'Old
  and (for all I in 1 .. Length (L) =>
            (if I in P.Get (Positions (L), First) .. P.Get (Positions (L), Last) then
               Element (Model (L), I) = 0
             else Element (Model (L), I) = Element (Model (L'Old), I)))
is
   Cu : Cursor := First;
begin
   loop
      pragma Loop_Invariant (Has_Element (L, Cu));
      pragma Loop_Invariant (P.Get (Positions (L), Cu) in P.Get (Positions (L), First) .. P.Get (Positions (L), Last));
      pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
      pragma Loop_Invariant (Positions (L) = Positions (L)'Loop_Entry);
      pragma Loop_Invariant (for all I in 1 .. Length (L) =>
                               (if I in P.Get (Positions (L), First) .. P.Get (Positions (L), Cu) - 1 then
                                   Element (Model (L), I) = 0
                                else Element (Model (L), I) = Element (Model (L'Loop_Entry), I)));
      Replace_Element (L, Cu, 0);
      exit when Cu = Last;
      Next (L, Cu);
   end loop;
end Update_Range_List_Zero;

Compared to the vector example, it requires three additional invariants. As the loop is done via a cursor, the first two loop invariants are necessary to know that the current cursor Cu stays between First and Last in the list. The fourth loop invariant states that the position of cursors in L is not modified during the loop. It is necessary to know that the two cursors First and Last keep designating the same range after the loop. With this loop invariant, GNATprove is able to prove the postcondition of Update_Range_List_Zero, namely that all elements between First and Last have been zeroed out, and that other elements have not been modified:

update_range_list_zero.adb:7:13: info: precondition proved
update_range_list_zero.adb:7:45: info: precondition proved
update_range_list_zero.adb:8:11: info: postcondition proved
update_range_list_zero.adb:11:23: info: precondition proved
update_range_list_zero.adb:11:55: info: precondition proved
update_range_list_zero.adb:12:16: info: precondition proved
update_range_list_zero.adb:13:19: info: precondition proved
update_range_list_zero.adb:13:44: info: precondition proved
update_range_list_zero.adb:18:30: info: loop invariant initialization proved
update_range_list_zero.adb:18:30: info: loop invariant preservation proved
update_range_list_zero.adb:18:46: info: initialization of "Cu.Node" proved
update_range_list_zero.adb:19:30: info: loop invariant initialization proved
update_range_list_zero.adb:19:30: info: loop invariant preservation proved
update_range_list_zero.adb:19:31: info: precondition proved
update_range_list_zero.adb:19:52: info: initialization of "Cu.Node" proved
update_range_list_zero.adb:19:60: info: precondition proved
update_range_list_zero.adb:19:92: info: precondition proved
update_range_list_zero.adb:20:30: info: loop invariant initialization proved
update_range_list_zero.adb:20:30: info: loop invariant preservation proved
update_range_list_zero.adb:21:30: info: loop invariant initialization proved
update_range_list_zero.adb:21:30: info: loop invariant preservation proved
update_range_list_zero.adb:22:30: info: loop invariant initialization proved
update_range_list_zero.adb:22:30: info: loop invariant preservation proved
update_range_list_zero.adb:23:42: info: precondition proved
update_range_list_zero.adb:23:74: info: precondition proved
update_range_list_zero.adb:23:95: info: initialization of "Cu.Node" proved
update_range_list_zero.adb:24:36: info: precondition proved
update_range_list_zero.adb:25:38: info: precondition proved
update_range_list_zero.adb:25:63: info: precondition proved
update_range_list_zero.adb:26:07: info: precondition proved
update_range_list_zero.adb:26:27: info: initialization of "Cu.Node" proved
update_range_list_zero.adb:27:17: info: initialization of "Cu.Node" proved
update_range_list_zero.adb:28:07: info: precondition proved
update_range_list_zero.adb:28:16: info: initialization of "Cu.Node" proved