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
:
1with SPARK.Containers.Formal.Doubly_Linked_Lists;
2with SPARK.Containers.Formal.Vectors;
3with SPARK.Big_Integers; use SPARK.Big_Integers;
4
5package Loop_Types
6 with SPARK_Mode
7is
8 subtype Index_T is Positive range 1 .. 1000;
9 subtype Opt_Index_T is Natural range 0 .. 1000;
10 subtype Component_T is Natural;
11
12 type Arr_T is array (Index_T) of Component_T;
13
14 package Vectors is new SPARK.Containers.Formal.Vectors (Index_T, Component_T);
15 subtype Vec_T is Vectors.Vector;
16
17 package Lists is new SPARK.Containers.Formal.Doubly_Linked_Lists (Component_T);
18 subtype List_T is Lists.List;
19
20 type List_Cell;
21 type List_Acc is access List_Cell;
22 type List_Cell is record
23 Value : Component_T;
24 Next : List_Acc;
25 end record;
26
27 function Length (L : access constant List_Cell) return Big_Natural is
28 (if L = null then 0 else Length (L.Next) + 1)
29 with Subprogram_Variant => (Structural => L);
30
31 function At_End
32 (L : access constant List_Cell) return access constant List_Cell
33 is (L)
34 with Ghost,
35 Annotate => (GNATprove, At_End_Borrow);
36
37 type Property is access function (X : Component_T) return Boolean;
38
39 function For_All_List
40 (L : access constant List_Cell;
41 P : not null Property) return Boolean
42 is
43 (L = null or else (P (L.Value) and then For_All_List (L.Next, P)))
44 with
45 Subprogram_Variant => (Structural => L);
46 pragma Annotate (GNATprove, False_Positive, "call via access-to-subprogram",
47 "We only call For_All_List on terminating functions");
48
49 type Relation is access function (X, Y : Component_T) return Boolean;
50
51 function For_All_List
52 (L1, L2 : access constant List_Cell;
53 P : not null Relation) return Boolean
54 is
55 ((L1 = null) = (L2 = null)
56 and then
57 (if L1 /= null
58 then P (L1.Value, L2.Value)
59 and then For_All_List (L1.Next, L2.Next, P)))
60 with
61 Subprogram_Variant => (Structural => L1);
62 pragma Annotate (GNATprove, False_Positive, "call via access-to-subprogram",
63 "We only call For_All_List on terminating functions");
64
65end Loop_Types;
As there is no built-in way to iterate over the elements of a recursive
data structure, the first function For_All_List
can be used to state that
all elements of a list have a given property. The second variant of
For_All_List
takes two lists and states that both lists have the same number
of elements and that the corresponding elements of both lists are related by the
given relation. The function At_End
is used to
refer to the value of a borrowed list or a local borrower at the end of the
borrow, see Annotation for Referring to a Value at the End of a Local Borrow for more
explanations.
Note
Although the structural subprogram variant of For_All_List
is proved,
this is not sufficient to prove the termination of For_All_List
,
as we have no way for now to state on
the access-to-subprogram type Property that all elements of this type
must terminate. Therefore, we justify this check, see section on
Justifying Check Messages.
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:
1procedure Increment_Loop (X : in out Integer; N : Natural) with
2 SPARK_Mode,
3 Pre => X <= Integer'Last - N,
4 Post => X = X'Old + N
5is
6begin
7 for I in 1 .. N loop
8 X := X + 1;
9 end loop;
10end 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:4:11: medium: postcondition might fail
4 | Post => X = X'Old + N
| ^~~~~~~~~~~~~
possible fix: loop at line 7 should mention X in a loop invariant
7 | for I in 1 .. N loop
| ^ here
increment_loop.adb:8:14: medium: overflow check might fail, cannot prove upper bound for X + 1
8 | X := X + 1;
| ~~^~~
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: loop at line 7 should mention X in a loop invariant
7 | for I in 1 .. N loop
| ^ here
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, as suggested
by the possible explanation in the message issued by GNATprove, that
describes precisely the value of X
in each iteration of the loop:
1procedure Increment_Loop_Inv (X : in out Integer; N : Natural) with
2 SPARK_Mode,
3 Pre => X <= Integer'Last - N,
4 Post => X = X'Old + N
5is
6begin
7 for I in 1 .. N loop
8 X := X + 1;
9 pragma Loop_Invariant (X = X'Loop_Entry + I);
10 end loop;
11end 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 preservation proved
increment_loop_inv.adb:9:30: info: loop invariant initialization 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, a container from the Formal Containers Library, or a pointer-based linked list).
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
:
1with Loop_Types; use Loop_Types;
2
3procedure Init_Arr_Zero (A : out Arr_T) with
4 SPARK_Mode,
5 Post => (for all J in A'Range => A(J) = 0)
6is
7 pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
8 "Entire array is initialized element-by-element in a loop");
9begin
10 for J in A'Range loop
11 A(J) := 0;
12 pragma Loop_Invariant (for all K in A'First .. J => A(K) = 0);
13 pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
14 "Part of array up to index J is initialized at this point");
15 end loop;
16end 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: justified that "A" might not be initialized in "Init_Arr_Zero"
init_arr_zero.adb:5:11: info: postcondition proved
init_arr_zero.adb:5:36: info: justified that "A" might not be initialized
init_arr_zero.adb:12:30: info: loop invariant initialization proved
init_arr_zero.adb:12:30: info: loop invariant preservation proved
init_arr_zero.adb:12:59: info: justified that "A" might not be initialized
init_arr_zero.adb:12:61: info: index check proved
In the example above, 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.
To verify this loop completely, it is possible to annotate A
with the
Relaxed_Initialization aspect to use proof to verify its correct initialization
(see Aspect Relaxed_Initialization and Ghost Attribute Initialized for more details).
In this case, the loop invariant should be extended to state that the elements
of A
have been initialized by the loop up to the current index:
1with Loop_Types; use Loop_Types;
2
3procedure Init_Arr_Zero (A : out Arr_T) with
4 SPARK_Mode,
5 Relaxed_Initialization => A,
6 Post => A'Initialized and then (for all J in A'Range => A(J) = 0)
7is
8begin
9 for J in A'Range loop
10 A(J) := 0;
11 pragma Loop_Invariant (for all K in A'First .. J => A(K)'Initialized);
12 pragma Loop_Invariant (for all K in A'First .. J => A(K) = 0);
13 end loop;
14end Init_Arr_Zero;
Remark that the postcondition of Init_Arr_Zero
also needs to state that
A
is entirely initialized by the call.
Consider now a variant of the same initialization loop over a vector:
1with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
2
3procedure Init_Vec_Zero (V : in out Vec_T) with
4 SPARK_Mode,
5 Post => (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0)
6is
7begin
8 for J in First_Index (V) .. Last_Index (V) loop
9 Replace_Element (V, J, 0);
10 pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
11 pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) = 0);
12 end loop;
13end 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:10:30: info: loop invariant preservation proved
init_vec_zero.adb:10:30: info: loop invariant initialization proved
init_vec_zero.adb:11:30: info: loop invariant preservation proved
init_vec_zero.adb:11:30: info: loop invariant initialization 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:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Init_List_Zero (L : in out List_T) with
5 SPARK_Mode,
6 Post => (for all E of L => E = 0)
7is
8 Cu : Cursor := First (L);
9begin
10 while Has_Element (L, Cu) loop
11 pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
12 Element (Model (L), I) = 0);
13 Replace_Element (L, Cu, 0);
14 Next (L, Cu);
15 end loop;
16end 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: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:12:32: info: precondition proved
init_list_zero.adb:13:07: info: precondition proved
init_list_zero.adb:14:07: info: precondition 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 variant of the same initialization loop over a pointer-based list:
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Is_Zero (X : Component_T) return Boolean is
7 (X = 0);
8
9 procedure Init_List_Zero (L : access List_Cell) with
10 Post => For_All_List (L, Is_Zero'Access);
11end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 procedure Init_List_Zero (L : access List_Cell) is
7 B : access List_Cell := L;
8 begin
9 while B /= null loop
10 pragma Loop_Invariant
11 (if For_All_List (At_End (B), Is_Zero'Access)
12 then For_All_List (At_End (L), Is_Zero'Access));
13 B.Value := 0;
14 B := B.Next;
15 end loop;
16 end Init_List_Zero;
17end P;
Like in the other variants, the postcondition of Init_List_Zero
states that
the elements of the list L
after the call are all 0
. It uses the
For_All_List
function from Loop_Types
to quantify over all the elements
of the list.
The loop iterates over the list L
using a local borrower B
which is
a local variable which borrows the ownership of a part of a datastructure for
the duration of its scope, see Borrowing for more details.
The loop invariant uses the At_End
function to express properties about the
values of L
and B
at the end of the borrow. It states that the elements
of L
at the end of the borrow will all be 0
if the elements of B
at
the end of the borrow are all 0
. This is provable because we know while
verifying the invariant that the already traversed elements were all set to
0
and that they can no longer be changed during the scope of B
. With
this loop invariant, GNATprove is able to prove the postcondition of
Init_List_Zero
:
p.adb:11:13: info: loop invariant initialization proved
p.adb:11:13: info: loop invariant preservation proved
p.adb:11:49: info: null exclusion check proved
p.adb:12:51: info: null exclusion check proved
p.adb:13:11: info: pointer dereference check proved
p.adb:14:16: info: pointer dereference check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Is_Zero" has been proved, subprogram will terminate
p.ads:10:14: info: postcondition proved
p.ads:10:38: info: null exclusion check proved
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:
1with Loop_Types; use Loop_Types;
2
3procedure Init_Arr_Index (A : out Arr_T) with
4 SPARK_Mode,
5 Post => (for all J in A'Range => A(J) = J)
6is
7 pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
8 "Entire array is initialized element-by-element in a loop");
9begin
10 for J in A'Range loop
11 A(J) := J;
12 pragma Loop_Invariant (for all K in A'First .. J => A(K) = K);
13 pragma Annotate (GNATprove, False_Positive, """A"" might not be initialized",
14 "Part of array up to index J is initialized at this point");
15 end loop;
16end 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: justified that "A" might not be initialized in "Init_Arr_Index"
init_arr_index.adb:5:11: info: postcondition proved
init_arr_index.adb:5:36: info: justified that "A" might not be initialized
init_arr_index.adb:12:30: info: loop invariant initialization proved
init_arr_index.adb:12:30: info: loop invariant preservation proved
init_arr_index.adb:12:59: info: justified that "A" might not be initialized
init_arr_index.adb:12:61: info: index check proved
As for Init_Arr_Zero
above, it is possible to annotate A
with the
Relaxed_Initialization aspect to use proof to verify its correct initialization:
1with Loop_Types; use Loop_Types;
2
3procedure Init_Arr_Index (A : out Arr_T) with
4 SPARK_Mode,
5 Relaxed_Initialization => A,
6 Post => A'Initialized and then (for all J in A'Range => A(J) = J)
7is
8begin
9 for J in A'Range loop
10 A(J) := J;
11 pragma Loop_Invariant (for all K in A'First .. J => A(K)'Initialized);
12 pragma Loop_Invariant (for all K in A'First .. J => A(K) = K);
13 end loop;
14end Init_Arr_Index;
Everything is proved by GNATprove:
init_arr_index.adb:6:11: info: postcondition proved
init_arr_index.adb:6:59: info: initialization check proved
init_arr_index.adb:11:30: info: loop invariant initialization proved
init_arr_index.adb:11:30: info: loop invariant preservation proved
init_arr_index.adb:11:61: info: index check proved
init_arr_index.adb:12:30: info: loop invariant preservation proved
init_arr_index.adb:12:30: info: loop invariant initialization proved
init_arr_index.adb:12:59: info: initialization check proved
init_arr_index.adb:12: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:
1with Loop_Types; use Loop_Types;
2
3procedure Map_Arr_Incr (A : in out Arr_T) with
4 SPARK_Mode,
5 Pre => (for all J in A'Range => A(J) /= Component_T'Last),
6 Post => (for all J in A'Range => A(J) = A'Old(J) + 1)
7is
8begin
9 for J in A'Range loop
10 A(J) := A(J) + 1;
11 pragma Loop_Invariant (for all K in A'First .. J => A(K) = A'Loop_Entry(K) + 1);
12 -- The following loop invariant is generated automatically by GNATprove:
13 -- pragma Loop_Invariant (for all K in J + 1 .. A'Last => A(K) = A'Loop_Entry(K));
14 end loop;
15end 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:
1pragma Unevaluated_Use_Of_Old (Allow);
2with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
3use Loop_Types.Vectors.Formal_Model;
4
5procedure Map_Vec_Incr (V : in out Vec_T) with
6 SPARK_Mode,
7 Pre => (for all I in 1 .. Last_Index (V) =>
8 Element (V, I) /= Component_T'Last),
9 Post => Last_Index (V) = Last_Index (V)'Old
10 and then (for all I in 1 .. Last_Index (V) =>
11 Element (V, I) = Element (Model (V)'Old, I) + 1)
12is
13begin
14 for J in 1 .. Last_Index (V) loop
15 pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
16 pragma Loop_Invariant
17 (for all I in 1 .. J - 1 =>
18 Element (V, I) = Element (Model (V)'Loop_Entry, I) + 1);
19 pragma Loop_Invariant
20 (for all I in J .. Last_Index (V) =>
21 Element (V, I) = Element (Model (V)'Loop_Entry, I));
22 Replace_Element (V, J, Element (V, J) + 1);
23 end loop;
24end 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:30: info: precondition proved
map_vec_incr.adb:22:45: info: overflow check proved
Similarly, consider a variant of the same mapping loop over a list:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Map_List_Incr (L : in out List_T) with
5 SPARK_Mode,
6 Pre => (for all E of L => E /= Component_T'Last),
7 Post => Length (L) = Length (L)'Old
8 and then (for all I in 1 .. Length (L) =>
9 Element (Model (L), I) = Element (Model (L'Old), I) + 1)
10is
11 Cu : Cursor := First (L);
12begin
13 while Has_Element (L, Cu) loop
14 pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
15 pragma Loop_Invariant
16 (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
17 Element (Model (L), I) = Element (Model (L'Loop_Entry), I) + 1);
18 pragma Loop_Invariant
19 (for all I in P.Get (Positions (L), Cu) .. Length (L) =>
20 Element (Model (L), I) = Element (Model (L'Loop_Entry), I));
21 Replace_Element (L, Cu, Element (L, Cu) + 1);
22 Next (L, Cu);
23 end loop;
24end 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: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: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: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 preservation proved
map_list_incr.adb:19:10: info: loop invariant initialization proved
map_list_incr.adb:19:24: info: precondition 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:31: info: precondition proved
map_list_incr.adb:21:47: info: overflow check proved
map_list_incr.adb:22:07: info: precondition proved
Finally, consider a variant of the same mapping loop over a pointer-based list:
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Small_Enough (X : Component_T) return Boolean is
7 (X /= Component_T'Last);
8 function Bigger_Than_First (X : Component_T) return Boolean is
9 (X /= Component_T'First);
10
11 procedure Map_List_Incr (L : access List_Cell) with
12 Pre => For_All_List (L, Small_Enough'Access),
13 Post => For_All_List (L, Bigger_Than_First'Access);
14end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 procedure Map_List_Incr (L : access List_Cell) is
7 B : access List_Cell := L;
8 begin
9 while B /= null loop
10 pragma Loop_Invariant (For_All_List (B, Small_Enough'Access));
11 pragma Loop_Invariant
12 (if For_All_List (At_End (B), Bigger_Than_First'Access)
13 then For_All_List (At_End (L), Bigger_Than_First'Access));
14 B.Value := B.Value + 1;
15 B := B.Next;
16 end loop;
17 end Map_List_Incr;
18end P;
Like in the other variants, the precondition of Map_List_Incr
states that
all elements of the input list L
are less than Component_T'Last
before
the call. It uses the For_All_List
function from Loop_Types
to
quantify over all the elements of the list. The postcondition is weaker than in
other variants of the loop. Indeed, referring to the value of a pointer-based
datastructure before the call is not allowed in the SPARK language.
Therefore we changed the postcondition to state instead that
all elements of the list are bigger than Component_T'First
after the call.
The loop iterates over the list L
using a local borrower B
which is
a local variable which borrows the ownership of a part of a datastructure for
the duration of its scope, see Borrowing for more details.
The loop invariant is made of two parts. The first one states that the initial
property still holds on the elements of L
accessible through B
. The
second uses the At_End
function to express properties about the values
of L
and B
at the end of the borrow. It states that the elements of
L
at the end of the borrow will have the Bigger_Than_First
property
if the elements of B
at the end of the borrow have this property. This is
provable because we know when verifying the invariant that the already traversed
elements currently have the Bigger_Than_First
property and that they can
no longer be changed during the scope of B
. With this
loop invariant, GNATprove is able to prove the postcondition of
Map_List_Incr
:
p.adb:10:33: info: loop invariant preservation proved
p.adb:10:33: info: loop invariant initialization proved
p.adb:10:62: info: null exclusion check proved
p.adb:12:13: info: loop invariant initialization proved
p.adb:12:13: info: loop invariant preservation proved
p.adb:12:59: info: null exclusion check proved
p.adb:13:61: info: null exclusion check proved
p.adb:14:11: info: pointer dereference check proved
p.adb:14:22: info: pointer dereference check proved
p.adb:14:29: info: overflow check proved
p.adb:15:16: info: pointer dereference check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Small_Enough" has been proved, subprogram will terminate
p.ads:8:13: info: implicit aspect Always_Terminates on "Bigger_Than_First" has been proved, subprogram will terminate
p.ads:12:43: info: null exclusion check proved
p.ads:13:14: info: postcondition proved
p.ads:13:48: info: null exclusion check proved
If we want to retain the most precise postcondition relating the elements of
the structure before and after the loop, we need to introduce a way to store
the values of the list before the call in a separate data structure. In the
following example, it is done by declaring a Copy
function which returns
a copy of its input list. In its postcondition, we use the two-valued
For_All_List
function to state that the elements of the new structure
are equal to the elements of the input structure. An alternative could be
to store the elements in a structure not subject to ownership like an array.
Note
The function Copy
is marked as Import
as it is not meant to be
executed. It could be implemented in SPARK by returning a deep copy of the
argument list, reallocating all cells of the list in the result.
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Small_Enough (X : Component_T) return Boolean is
7 (X /= Component_T'Last);
8
9 function Equal (X, Y : Component_T) return Boolean is (X = Y);
10
11 function Is_Incr (X, Y : Component_T) return Boolean is
12 (X < Y and then Y = X + 1);
13
14 function Copy (L : access List_Cell) return List_Acc with
15 Ghost,
16 Import,
17 Global => null,
18 Post => For_All_List (L, Copy'Result, Equal'Access);
19
20 procedure Map_List_Incr (L : access List_Cell) with
21 Pre => For_All_List (L, Small_Enough'Access),
22 Post => For_All_List (Copy (L)'Old, L, Is_Incr'Access);
23 pragma Annotate (GNATprove, Intentional, "memory leak might occur",
24 "The code will be compiled with assertions disabled");
25end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 procedure Map_List_Incr (L : access List_Cell) is
7 L_Old : constant List_Acc := Copy (L) with Ghost;
8 pragma Annotate (GNATprove, Intentional, "memory leak might occur",
9 "The code will be compiled with assertions disabled");
10 B : access List_Cell := L;
11 B_Old : access constant List_Cell := L_Old with Ghost;
12 begin
13 while B /= null loop
14 pragma Loop_Invariant (For_All_List (B, Small_Enough'Access));
15 pragma Loop_Invariant (For_All_List (B, B_Old, Equal'Access));
16 pragma Loop_Invariant
17 (if For_All_List (B_Old, At_End (B), Is_Incr'Access)
18 then For_All_List (L_Old, At_End (L), Is_Incr'Access));
19 B.Value := B.Value + 1;
20 B := B.Next;
21 B_Old := B_Old.Next;
22 end loop;
23 pragma Assert
24 (For_All_List (L_Old, At_End (L), Is_Incr'Access));
25 end Map_List_Incr;
26end P;
The postcondition of Map_List_Incr
is similar to the postcondition of
Copy
. It uses the two-valued For_All_List
function to relate the
elements of L
before and after the call. Like in the previous variant, the
loop traverses L
using a local borrower B
. To be able to speak
about the initial value of L
in the invariant, we introduce a ghost
constant L_Old
storing a copy of this value. As we need to traverse both
lists at the same time, we declare a ghost variable B_Old
as a local
observer of L_Old
.
The loop invariant is made of three parts now. The first one is similar to the
one in the previous example. The third loop invariant is a direct adaptation of
the second loop invariant of the previous example. It states that if, at the end
of the borrow, the values accessible through B
are related to their
equivalent element in B_Old
through Is_Incr
, then so are all the
elements of L
. The loop invariant in the middle states that the elements
reachable through B
have not been modified by the loop. GNATprove can
verify these loop invariants as well as the postcondition of Map_List_Incr
:
p.adb:7:07: info: absence of resource or memory leak at end of scope justified
p.adb:14:33: info: loop invariant initialization proved
p.adb:14:33: info: loop invariant preservation proved
p.adb:14:62: info: null exclusion check proved
p.adb:15:33: info: loop invariant initialization proved
p.adb:15:33: info: loop invariant preservation proved
p.adb:15:62: info: null exclusion check proved
p.adb:17:13: info: loop invariant initialization proved
p.adb:17:13: info: loop invariant preservation proved
p.adb:17:56: info: null exclusion check proved
p.adb:18:58: info: null exclusion check proved
p.adb:19:11: info: pointer dereference check proved
p.adb:19:22: info: pointer dereference check proved
p.adb:19:29: info: overflow check proved
p.adb:20:16: info: pointer dereference check proved
p.adb:21:24: info: pointer dereference check proved
p.adb:24:10: info: assertion proved
p.adb:24:50: info: null exclusion check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Small_Enough" has been proved, subprogram will terminate
p.ads:9:13: info: implicit aspect Always_Terminates on "Equal" has been proved, subprogram will terminate
p.ads:11:13: info: implicit aspect Always_Terminates on "Is_Incr" has been proved, subprogram will terminate
p.ads:12:28: info: overflow check proved
p.ads:21:43: info: null exclusion check proved
p.ads:22:14: info: postcondition proved
p.ads:22:28: info: absence of resource or memory leak justified
p.ads:22:52: info: null exclusion check proved
Note
The second loop invariant does not subsume the first. Indeed, proving that,
if all elements of L_Old
are small enough, so are all elements of an
unknown observer B_Old
of L_Old
, is beyond the capacity of
GNATprove.
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:
1with Loop_Types; use Loop_Types;
2
3procedure Validate_Arr_Zero (A : Arr_T; Success : out Boolean) with
4 SPARK_Mode,
5 Post => Success = (for all J in A'Range => A(J) = 0)
6is
7begin
8 for J in A'Range loop
9 if A(J) /= 0 then
10 Success := False;
11 return;
12 end if;
13 pragma Loop_Invariant (for all K in A'First .. J => A(K) = 0);
14 end loop;
15
16 Success := True;
17end 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: 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:
1with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
2
3procedure Validate_Vec_Zero (V : Vec_T; Success : out Boolean) with
4 SPARK_Mode,
5 Post => Success = (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0)
6is
7begin
8 for J in First_Index (V) .. Last_Index (V) loop
9 if Element (V, J) /= 0 then
10 Success := False;
11 return;
12 end if;
13 pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) = 0);
14 end loop;
15
16 Success := True;
17end 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: 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: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:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Validate_List_Zero (L : List_T; Success : out Boolean) with
5 SPARK_Mode,
6 Post => Success = (for all E of L => E = 0)
7is
8 Cu : Cursor := First (L);
9begin
10 while Has_Element (L, Cu) loop
11 pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
12 Element (Model (L), I) = 0);
13 if Element (L, Cu) /= 0 then
14 Success := False;
15 return;
16 end if;
17 Next (L, Cu);
18 end loop;
19
20 Success := True;
21end 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: postcondition 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:12:32: info: precondition proved
validate_list_zero.adb:13:10: info: precondition proved
validate_list_zero.adb:17:07: info: precondition proved
The case of sets and maps is similar to the case of lists.
Consider now a variant of the same validation loop over a pointer-based list:
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Is_Zero (X : Component_T) return Boolean is
7 (X = 0);
8
9 procedure Validate_List_Zero
10 (L : access constant List_Cell;
11 Success : out Boolean)
12 with
13 Post => Success = For_All_List (L, Is_Zero'Access);
14end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 procedure Validate_List_Zero
7 (L : access constant List_Cell;
8 Success : out Boolean)
9 is
10 C : access constant List_Cell := L;
11 begin
12 while C /= null loop
13 pragma Loop_Invariant
14 (For_All_List (L, Is_Zero'Access) = For_All_List (C, Is_Zero'Access));
15 if C.Value /= 0 then
16 Success := False;
17 return;
18 end if;
19 C := C.Next;
20 end loop;
21
22 Success := True;
23 end Validate_List_Zero;
24end P;
The loop is implemented using a local observer (see Observing) which
borrows a read-only permission over a part of a datastructure until the end
of the scope of the observer. In the loop invariant, we cannot, like in
the other versions of the algorithm, speak about the value of the elements
which have already been traversed to say that they are all 0
. Instead,
we state that the list L
only contains 0
iff C
only contains 0
.
This is true since the loop exits as soon as a non-zero value is encountered.
With this invariant, the postcondition can be proved by GNATprove:
p.adb:14:13: info: loop invariant initialization proved
p.adb:14:13: info: loop invariant preservation proved
p.adb:14:37: info: null exclusion check proved
p.adb:14:72: info: null exclusion check proved
p.adb:15:14: info: pointer dereference check proved
p.adb:19:16: info: pointer dereference check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Is_Zero" has been proved, subprogram will terminate
p.ads:11:07: info: initialization of "Success" proved
p.ads:13:14: info: postcondition proved
p.ads:13:48: info: null exclusion check proved
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:
1with Loop_Types; use Loop_Types;
2
3procedure Validate_Full_Arr_Zero (A : Arr_T; Success : out Boolean) with
4 SPARK_Mode,
5 Post => Success = (for all J in A'Range => A(J) = 0)
6is
7begin
8 Success := True;
9
10 for J in A'Range loop
11 if A(J) /= 0 then
12 Success := False;
13 -- perform some logging here instead of returning
14 end if;
15 pragma Loop_Invariant (Success = (for all K in A'First .. J => A(K) = 0));
16 end loop;
17end 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: postcondition 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
:
1with Loop_Types; use Loop_Types;
2
3procedure Count_Arr_Zero (A : Arr_T; Counter : out Natural) with
4 SPARK_Mode,
5 Post => (Counter in 0 .. A'Length) and then
6 ((Counter = 0) = (for all K in A'Range => A(K) /= 0))
7is
8begin
9 Counter := 0;
10
11 for J in A'Range loop
12 if A(J) = 0 then
13 Counter := Counter + 1;
14 end if;
15 pragma Loop_Invariant (Counter in 0 .. J);
16 pragma Loop_Invariant ((Counter = 0) = (for all K in A'First .. J => A(K) /= 0));
17 end loop;
18end 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:13:29: info: overflow check 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 preservation proved
count_arr_zero.adb:16:30: info: loop invariant initialization proved
count_arr_zero.adb:16:78: info: index check proved
Consider now a variant of the same counting loop over a vector:
1with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
2
3procedure Count_Vec_Zero (V : Vec_T; Counter : out Natural) with
4 SPARK_Mode,
5 Post => (Counter in 0 .. Natural (Length (V))) and then
6 ((Counter = 0) = (for all K in First_Index (V) .. Last_Index (V) => Element (V, K) /= 0))
7is
8begin
9 Counter := 0;
10
11 for J in First_Index (V) .. Last_Index (V) loop
12 if Element (V, J) = 0 then
13 Counter := Counter + 1;
14 end if;
15 pragma Loop_Invariant (Counter in 0 .. J);
16 pragma Loop_Invariant ((Counter = 0) = (for all K in First_Index (V) .. J => Element (V, K) /= 0));
17 end loop;
18end 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: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:13:29: info: overflow check 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: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
:
1with Loop_Types; use Loop_Types;
2
3procedure Search_Arr_Zero (A : Arr_T; Pos : out Opt_Index_T; Success : out Boolean) with
4 SPARK_Mode,
5 Post => Success = (for some J in A'Range => A(J) = 0) and then
6 (if Success then A (Pos) = 0)
7is
8begin
9 for J in A'Range loop
10 if A(J) = 0 then
11 Success := True;
12 Pos := J;
13 return;
14 end if;
15 pragma Loop_Invariant (for all K in A'First .. J => A(K) /= 0);
16 end loop;
17
18 Success := False;
19 Pos := 0;
20end 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: postcondition proved
search_arr_zero.adb:6:31: info: index check 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:
1with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
2
3procedure Search_Vec_Zero (V : Vec_T; Pos : out Opt_Index_T; Success : out Boolean) with
4 SPARK_Mode,
5 Post => Success = (for some J in First_Index (V) .. Last_Index (V) => Element (V, J) = 0) and then
6 (if Success then Element (V, Pos) = 0)
7is
8begin
9 for J in First_Index (V) .. Last_Index (V) loop
10 if Element (V, J) = 0 then
11 Success := True;
12 Pos := J;
13 return;
14 end if;
15 pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) /= 0);
16 end loop;
17
18 Success := False;
19 Pos := 0;
20end 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: 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:28: info: precondition proved
search_vec_zero.adb:10:10: info: precondition proved
search_vec_zero.adb:15:30: info: loop invariant preservation proved
search_vec_zero.adb:15:30: info: loop invariant initialization 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:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Search_List_Zero (L : List_T; Pos : out Cursor; Success : out Boolean) with
5 SPARK_Mode,
6 Post => Success = (for some E of L => E = 0) and then
7 (if Success then Element (L, Pos) = 0)
8is
9 Cu : Cursor := First (L);
10begin
11 while Has_Element (L, Cu) loop
12 pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
13 Element (Model (L), I) /= 0);
14 if Element (L, Cu) = 0 then
15 Success := True;
16 Pos := Cu;
17 return;
18 end if;
19 Next (L, Cu);
20 end loop;
21
22 Success := False;
23 Pos := No_Element;
24end 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" proved
search_list_zero.adb:4:59: info: initialization of "Success" proved
search_list_zero.adb:6:11: info: postcondition proved
search_list_zero.adb:7:28: info: precondition 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:13:32: info: precondition proved
search_list_zero.adb:14:10: info: precondition proved
search_list_zero.adb:19:07: info: precondition proved
The case of sets and maps is similar to the case of lists.
Consider a variant of the same search loop over a pointer-based list:
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Is_Non_Zero (X : Component_T) return Boolean is
7 (X /= 0);
8
9 function Search_List_Zero (L : access List_Cell) return access List_Cell with
10 Post =>
11 ((Search_List_Zero'Result = null) = For_All_List (L, Is_Non_Zero'Access)
12 and then
13 (if Search_List_Zero'Result /= null then Search_List_Zero'Result.Value = 0));
14end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 function Search_List_Zero (L : access List_Cell) return access List_Cell is
7 B : access List_Cell := L;
8 begin
9 while B /= null and then B.Value /= 0 loop
10 pragma Loop_Variant (Structural => B);
11 pragma Loop_Invariant
12 (For_All_List (L, Is_Non_Zero'Access) =
13 For_All_List (B, Is_Non_Zero'Access));
14 B := B.Next;
15 end loop;
16
17 return B;
18 end Search_List_Zero;
19end P;
As our pointer-based lists do not support cursors, the result of the search
is a pointer inside the list which can be used to access or even update the
corresponding element. Storing such an object inside an OUT parameter would
break the ownership model of SPARK by creating an alias. Instead, we use a
traversal function (see Traversal Functions) to return this pointer
as a local borrower of the input list. Since we now have a function, we can
no longer have an explicit Success
flag to encode whether or not the value
was found. Instead, we simply return null
in case of failure.
The loop iterates over the input list L
using a local borrower B
. The
iteration stops when either B
is null
or B.Value
is zero. In the
loop invariant, we cannot speak directly about the elements of L
that have
been traversed to say that they are not 0
. Instead, we write in the
invariant that L
contains only non-zero values iff B
contains only
non-zero values. Thanks to this loop invariant, GNATprove is able to verify
the postcondition of Search_List_Zero
:
p.adb:9:33: info: pointer dereference check proved
p.adb:10:10: info: loop variant proved
p.adb:12:13: info: loop invariant initialization proved
p.adb:12:13: info: loop invariant preservation proved
p.adb:12:41: info: null exclusion check proved
p.adb:13:45: info: null exclusion check proved
p.adb:14:16: info: pointer dereference check proved
p.adb:17:14: info: dynamic accessibility check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Is_Non_Zero" has been proved, subprogram will terminate
p.ads:9:13: info: implicit aspect Always_Terminates on "Search_List_Zero" has been proved, subprogram will terminate
p.ads:11:08: info: postcondition proved
p.ads:11:72: info: null exclusion check proved
p.ads:13:77: info: pointer dereference check proved
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
:
1with Loop_Types; use Loop_Types;
2
3procedure Search_Arr_Max (A : Arr_T; Pos : out Index_T; Max : out Component_T) with
4 SPARK_Mode,
5 Post => (for all J in A'Range => A(J) <= Max) and then
6 (for some J in A'Range => A(J) = Max) and then
7 A(Pos) = Max
8is
9begin
10 Max := 0;
11 Pos := A'First;
12
13 for J in A'Range loop
14 if A(J) > Max then
15 Max := A(J);
16 Pos := J;
17 end if;
18 pragma Loop_Invariant (for all K in A'First .. J => A(K) <= Max);
19 pragma Loop_Invariant (for some K in A'First .. J => A(K) = Max);
20 pragma Loop_Invariant (A(Pos) = Max);
21 end loop;
22end 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: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:19:30: info: loop invariant preservation proved
search_arr_max.adb:19:30: info: loop invariant initialization proved
search_arr_max.adb:19:62: info: index check proved
search_arr_max.adb:20:30: info: loop invariant initialization proved
search_arr_max.adb:20:30: info: loop invariant preservation proved
Consider now a variant of the same search loop over a vector:
1with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
2
3procedure Search_Vec_Max (V : Vec_T; Pos : out Index_T; Max : out Component_T) with
4 SPARK_Mode,
5 Pre => not Is_Empty (V),
6 Post => (for all J in First_Index (V) .. Last_Index (V) => Element (V, J) <= Max) and then
7 (for some J in First_Index (V) .. Last_Index (V) => Element (V, J) = Max) and then
8 Pos in First_Index (V) .. Last_Index (V) and then
9 Element (V, Pos) = Max
10is
11begin
12 Max := 0;
13 Pos := First_Index (V);
14
15 for J in First_Index (V) .. Last_Index (V) loop
16 if Element (V, J) > Max then
17 Max := Element (V, J);
18 Pos := J;
19 end if;
20 pragma Loop_Invariant (for all K in First_Index (V) .. J => Element (V, K) <= Max);
21 pragma Loop_Invariant (for some K in First_Index (V) .. J => Element (V, K) = Max);
22 pragma Loop_Invariant (Pos in First_Index (V) .. J);
23 pragma Loop_Invariant (Element (V, Pos) = Max);
24 end loop;
25end 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:7:63: info: precondition proved
search_vec_max.adb:7:75: info: range check proved
search_vec_max.adb:9:11: info: precondition proved
search_vec_max.adb:16:10: info: precondition proved
search_vec_max.adb:17:17: info: precondition 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: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:22:30: info: loop invariant preservation proved
search_vec_max.adb:22:30: info: loop invariant initialization proved
search_vec_max.adb:23:30: info: precondition proved
search_vec_max.adb:23:30: info: loop invariant preservation proved
search_vec_max.adb:23:30: info: loop invariant initialization proved
Similarly, consider a variant of the same search loop over a list:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Search_List_Max (L : List_T; Pos : out Cursor; Max : out Component_T) with
5 SPARK_Mode,
6 Pre => not Is_Empty (L),
7 Post => (for all E of L => E <= Max) and then
8 (for some E of L => E = Max) and then
9 Has_Element (L, Pos) and then
10 Element (L, Pos) = Max
11is
12 Cu : Cursor := First (L);
13begin
14 Max := 0;
15 Pos := Cu;
16
17 while Has_Element (L, Cu) loop
18 pragma Loop_Invariant (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
19 Element (Model (L), I) <= Max);
20 pragma Loop_Invariant (Has_Element (L, Pos));
21 pragma Loop_Invariant (Max = 0 or else Element (L, Pos) = Max);
22
23 if Element (L, Cu) > Max then
24 Max := Element (L, Cu);
25 Pos := Cu;
26 end if;
27 Next (L, Cu);
28 end loop;
29end 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" 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:10:11: info: precondition proved
search_list_max.adb:18:30: info: loop invariant preservation proved
search_list_max.adb:18:30: info: loop invariant initialization proved
search_list_max.adb:18:49: info: precondition proved
search_list_max.adb:19:32: info: precondition 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: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:23:10: info: precondition proved
search_list_max.adb:24:17: info: precondition proved
search_list_max.adb:27:07: info: precondition proved
The case of sets and maps is similar to the case of lists.
Consider a variant of the same search loop over a pointer-based list:
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function All_Smaller_Than_Max
7 (L : access constant List_Cell; Max : Component_T) return Boolean
8 is (L = null or else
9 (L.Value <= Max and then All_Smaller_Than_Max (L.Next, Max)))
10 with
11 Subprogram_Variant => (Structural => L);
12
13 function Search_List_Max
14 (L : not null access List_Cell) return not null access List_Cell
15 with
16 Post => All_Smaller_Than_Max (L, Search_List_Max'Result.Value);
17end P;
1with Loop_Types; use Loop_Types;
2with SPARK.Big_Integers; use SPARK.Big_Integers;
3
4package body P with
5 SPARK_Mode
6is
7 function Search_List_Max
8 (L : not null access List_Cell) return not null access List_Cell
9 is
10 B : access List_Cell := L;
11 begin
12 loop
13 pragma Loop_Invariant (B /= null);
14 pragma Loop_Invariant
15 (for all M in B.Value .. Component_T'Last =>
16 (if All_Smaller_Than_Max (B, M)
17 then All_Smaller_Than_Max (L, M)));
18 pragma Loop_Variant (Decreases => Length (B));
19 declare
20 Prec : access List_Cell := B;
21 Max : constant Component_T := B.Value;
22 begin
23 loop
24 B := B.Next;
25 exit when B = null or else B.Value > Max;
26 pragma Loop_Invariant (B /= null);
27 pragma Loop_Invariant (B.Value <= Max);
28 pragma Loop_Invariant (Length (B) < Length (B)'Loop_Entry);
29 pragma Loop_Invariant
30 (for all M in Max .. Component_T'Last =>
31 (if All_Smaller_Than_Max (B, M)
32 then All_Smaller_Than_Max (L, M)));
33 pragma Loop_Variant (Decreases => Length (B));
34 end loop;
35 if B = null then
36 return Prec;
37 end if;
38 end;
39 end loop;
40 end Search_List_Max;
41end P;
As our pointer-based lists do not support cursors, the result of the search
is a pointer inside the list which can be used to access or even update the
corresponding element. Storing such an object inside an OUT parameter would
break the ownership model of SPARK by creating an alias. Instead, we use a
traversal function (see Traversal Functions) to return this pointer
as a local borrower of the input list. Since we now have a function, we can
no longer explicitely return the value of the maximum. It is not a problem,
as it can be accessed easily as the Value
component of the returned
pointer. In the postcondition of Search_List_Max
, we cannot use
For_All_List
to express that the returned pointer designates the maximum
value in the list. Indeed, the property depends on the value of this maximum.
Instead, we create a specific recursive function taking the maximum as an
additional parameter.
The iteration over the input list L
uses a local borrower B
. It is
expressed as two nested loops. The inner loop declares a local borrower Prec
to register the current value of the maximum. Then it iterates through the loop
using B
until a value bigger than the current maximum is found. The outer
loop repeats this step as many times as necessary. This split into two loops
is necessary as the SPARK language prevents borrowers from jumping into a
different part of the data structure. As B
is not syntactically a path
rooted at Prec
, Prec
cannot be assigned the current value of B
when
a new maximal value is found. We therefore need to create a new variable
to hold the current maximum each time it changes.
In the loop invariant of the outer loop, we cannot speak directly about the
elements of L
that have been traversed to say that they are smaller than
the current maximum. Instead, we write in the invariant that the all values of
L
are smaller than any given value bigger than the current maximum iff the
values of B
are. A similar invariant is necessary on the inner loop.
Thanks to these loop invariants, GNATprove is able to verify
the postcondition of Search_List_Max
:
p.adb:13:33: info: loop invariant preservation proved
p.adb:13:33: info: loop invariant initialization proved
p.adb:15:13: info: loop invariant initialization proved
p.adb:15:13: info: loop invariant preservation proved
p.adb:15:27: info: pointer dereference check proved
p.adb:16:44: info: range check proved
p.adb:17:46: info: range check proved
p.adb:18:31: info: loop variant proved
p.adb:18:44: info: range check proved
p.adb:21:45: info: pointer dereference check proved
p.adb:24:22: info: pointer dereference check proved
p.adb:25:44: info: pointer dereference check proved
p.adb:26:39: info: loop invariant initialization proved
p.adb:26:39: info: loop invariant preservation proved
p.adb:27:39: info: loop invariant initialization proved
p.adb:27:39: info: loop invariant preservation proved
p.adb:27:40: info: pointer dereference check proved
p.adb:28:39: info: predicate check proved
p.adb:28:39: info: loop invariant initialization proved
p.adb:28:39: info: loop invariant preservation proved
p.adb:28:62: info: predicate check proved
p.adb:30:19: info: loop invariant initialization proved
p.adb:30:19: info: loop invariant preservation proved
p.adb:31:50: info: range check proved
p.adb:32:52: info: range check proved
p.adb:33:37: info: loop variant proved
p.adb:33:50: info: range check proved
p.adb:36:23: info: dynamic accessibility check proved
p.adb:36:23: info: null exclusion check proved
p.ads:6:13: info: implicit aspect Always_Terminates on "All_Smaller_Than_Max" has been proved, subprogram will terminate
p.ads:9:12: info: pointer dereference check proved
p.ads:9:35: info: subprogram variant proved
p.ads:9:58: info: pointer dereference check proved
p.ads:13:13: info: implicit aspect Always_Terminates on "Search_List_Max" has been proved, subprogram will terminate
p.ads:16:14: info: postcondition proved
The loop variants state that the length of B
is strictly
decreasing. This is used to prove that the loop terminates.
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
:
1with Loop_Types; use Loop_Types;
2
3procedure Update_Arr_Zero (A : in out Arr_T; Threshold : Component_T) with
4 SPARK_Mode,
5 Post => (for all J in A'Range => A(J) = (if A'Old(J) <= Threshold then 0 else A'Old(J)))
6is
7begin
8 for J in A'Range loop
9 if A(J) <= Threshold then
10 A(J) := 0;
11 end if;
12 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)));
13 -- The following loop invariant is generated automatically by GNATprove:
14 -- pragma Loop_Invariant (for all K in J + 1 .. A'Last => A(K) = A'Loop_Entry(K));
15 end loop;
16end 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:
1pragma Unevaluated_Use_Of_Old (Allow);
2with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
3use Loop_Types.Vectors.Formal_Model;
4
5procedure Update_Vec_Zero (V : in out Vec_T; Threshold : Component_T) with
6 SPARK_Mode,
7 Post => Last_Index (V) = Last_Index (V)'Old
8 and (for all I in 1 .. Last_Index (V) =>
9 Element (V, I) =
10 (if Element (Model (V)'Old, I) <= Threshold then 0
11 else Element (Model (V)'Old, I)))
12is
13begin
14 for J in First_Index (V) .. Last_Index (V) loop
15 pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
16 pragma Loop_Invariant
17 (for all I in 1 .. J - 1 =>
18 Element (V, I) =
19 (if Element (Model (V)'Loop_Entry, I) <= Threshold then 0
20 else Element (Model (V)'Loop_Entry, I)));
21 pragma Loop_Invariant
22 (for all I in J .. Last_Index (V) =>
23 Element (V, I) = Element (Model (V)'Loop_Entry, I));
24 if Element (V, J) <= Threshold then
25 Replace_Element (V, J, 0);
26 end if;
27 end loop;
28end 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:25:10: info: precondition proved
Similarly, consider a variant of the same update loop over a list:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Update_List_Zero (L : in out List_T; Threshold : Component_T) with
5 SPARK_Mode,
6 Post => Length (L) = Length (L)'Old
7 and (for all I in 1 .. Length (L) =>
8 Element (Model (L), I) =
9 (if Element (Model (L'Old), I) <= Threshold then 0
10 else Element (Model (L'Old), I)))
11is
12 Cu : Cursor := First (L);
13begin
14 while Has_Element (L, Cu) loop
15 pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
16 pragma Loop_Invariant
17 (for all I in 1 .. P.Get (Positions (L), Cu) - 1 =>
18 Element (Model (L), I) =
19 (if Element (Model (L'Loop_Entry), I) <= Threshold then 0
20 else Element (Model (L'Loop_Entry), I)));
21 pragma Loop_Invariant
22 (for all I in P.Get (Positions (L), Cu) .. Length (L) =>
23 Element (Model (L), I) = Element (Model (L'Loop_Entry), I));
24 if Element (L, Cu) <= Threshold then
25 Replace_Element (L, Cu, 0);
26 end if;
27 Next (L, Cu);
28 end loop;
29end 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: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 preservation proved
update_list_zero.adb:17:10: info: loop invariant initialization proved
update_list_zero.adb:17:29: info: precondition 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 preservation proved
update_list_zero.adb:22:10: info: loop invariant initialization proved
update_list_zero.adb:22:24: info: precondition 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:25:10: info: precondition proved
update_list_zero.adb:27:07: info: precondition proved
The case of sets and maps is similar to the case of lists.
Consider now a variant of the same update loop over a pointer-based list.
To express the postcondition relating the elements of the structure before and
after the loop, we need to introduce a way to store the values of the list
before the call in a separate data structure. Indeed, the Old
attribute
cannot be used on L
directly has it would introduce an alias. In this
example, it is done by declaring a Copy
function which returns
a copy of its input list. In its postcondition, we use the two-valued
For_All_List
function to state that the elements of the new structure
are equal to the elements of its input structure. An alternative could be
to store the elements in a structure not subject to ownership like an array.
Note
The function Copy
is marked as Import
as it is not meant to be
executed. It could be implemented in SPARK by returning a deep copy of the
argument list, reallocating all cells of the list in the result.
1with Loop_Types; use Loop_Types;
2
3package P with
4 SPARK_Mode
5is
6 function Equal (X, Y : Component_T) return Boolean is (X = Y);
7
8 function Copy (L : access List_Cell) return List_Acc with
9 Ghost,
10 Import,
11 Global => null,
12 Post => For_All_List (L, Copy'Result, Equal'Access);
13
14 function Updated_If_Less_Than_Threshold
15 (L1, L2 : access constant List_Cell;
16 Threshold : Component_T) return Boolean
17 is
18 ((L1 = null) = (L2 = null)
19 and then
20 (if L1 /= null then
21 (if L1.Value <= Threshold then L2.Value = 0
22 else L2.Value = L1.Value)
23 and then Updated_If_Less_Than_Threshold (L1.Next, L2.Next, Threshold)))
24 with
25 Subprogram_Variant => (Structural => L1);
26
27 procedure Update_List_Zero (L : access List_Cell; Threshold : Component_T) with
28 Post => Updated_If_Less_Than_Threshold (Copy (L)'Old, L, Threshold);
29 pragma Annotate (GNATprove, Intentional, "memory leak might occur",
30 "The code will be compiled with assertions disabled");
31end P;
1with Loop_Types; use Loop_Types;
2
3package body P with
4 SPARK_Mode
5is
6 procedure Update_List_Zero (L : access List_Cell; Threshold : Component_T) is
7 L_Old : constant List_Acc := Copy (L) with Ghost;
8 pragma Annotate (GNATprove, Intentional, "memory leak might occur",
9 "The code will be compiled with assertions disabled");
10 B : access List_Cell := L;
11 B_Old : access constant List_Cell := L_Old with Ghost;
12 begin
13 while B /= null loop
14 pragma Loop_Invariant (For_All_List (B, B_Old, Equal'Access));
15 pragma Loop_Invariant
16 (if Updated_If_Less_Than_Threshold (B_Old, At_End (B), Threshold)
17 then Updated_If_Less_Than_Threshold (L_Old, At_End (L), Threshold));
18 if B.Value <= Threshold then
19 B.Value := 0;
20 end if;
21 B := B.Next;
22 B_Old := B_Old.Next;
23 end loop;
24 pragma Assert
25 (Updated_If_Less_Than_Threshold (L_Old, At_End (L), Threshold));
26 end Update_List_Zero;
27end P;
In the postcondition of Update_List_Zero
, we cannot use For_All_List
to
express the relation between the values of the list before and after the call.
Indeed, the relation depends on the value of the input Threshold
.
Instead, we create a specific recursive function taking the threshold as an
additional parameter.
The loop traverses L
using a local borrower B
. To be able to speak
about the initial value of L
in the invariant, we introduce a ghost
constant L_Old
storing a copy of this value. As we need to traverse both
lists at the same time, we declare a ghost variable B_Old
as a local
observer of L_Old
.
The loop invariant is made of two parts. The first one states that the elements
reachable through B
have not been modified by the loop. In the second loop
invariant, we want to use Updated_If_Less_Than_Threshold
to relate the
elements of L
that were already traversed to the elements of L_Old
.
As we cannot speak specifically about the traversed elements of L
, the
invariant states that, if at the end of the borrow the values accessible
through B
are related to their equivalent element in B_Old
through
Updated_If_Less_Than_Threshold
, then so are all the elements of L
.
GNATprove can verify these invariants as well as the postcondition of
Update_List_Zero
:
p.adb:7:07: info: absence of resource or memory leak at end of scope justified
p.adb:14:33: info: loop invariant initialization proved
p.adb:14:33: info: loop invariant preservation proved
p.adb:14:62: info: null exclusion check proved
p.adb:16:13: info: loop invariant initialization proved
p.adb:16:13: info: loop invariant preservation proved
p.adb:18:14: info: pointer dereference check proved
p.adb:19:14: info: pointer dereference check proved
p.adb:21:16: info: pointer dereference check proved
p.adb:22:24: info: pointer dereference check proved
p.adb:25:10: info: assertion proved
p.ads:6:13: info: implicit aspect Always_Terminates on "Equal" has been proved, subprogram will terminate
p.ads:14:13: info: implicit aspect Always_Terminates on "Updated_If_Less_Than_Threshold" has been proved, subprogram will terminate
p.ads:21:20: info: pointer dereference check proved
p.ads:21:47: info: pointer dereference check proved
p.ads:22:22: info: pointer dereference check proved
p.ads:22:33: info: pointer dereference check proved
p.ads:23:19: info: subprogram variant proved
p.ads:23:53: info: pointer dereference check proved
p.ads:23:62: info: pointer dereference check proved
p.ads:28:14: info: postcondition proved
p.ads:28:46: info: absence of resource or memory leak justified
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
:
1with Loop_Types; use Loop_Types;
2
3procedure Update_Range_Arr_Zero (A : in out Arr_T; First, Last : Index_T) with
4 SPARK_Mode,
5 Post => A = (A'Old with delta First .. Last => 0)
6is
7begin
8 for J in First .. Last loop
9 A(J) := 0;
10 pragma Loop_Invariant (A = (A'Loop_Entry with delta First .. J => 0));
11 end loop;
12end 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
Delta Aggregates 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
Consider now a variant of the same update loop over a vector:
1pragma Unevaluated_Use_Of_Old (Allow);
2with Loop_Types; use Loop_Types; use Loop_Types.Vectors;
3use Loop_Types.Vectors.Formal_Model;
4
5procedure Update_Range_Vec_Zero (V : in out Vec_T; First, Last : Index_T) with
6 SPARK_Mode,
7 Pre => Last <= Last_Index (V),
8 Post => (for all J in 1 .. Last_Index (V) =>
9 (if J in First .. Last then Element (V, J) = 0
10 else Element (V, J) = Element (Model (V)'Old, J)))
11is
12begin
13 for J in First .. Last loop
14 Replace_Element (V, J, 0);
15 pragma Loop_Invariant (Last_Index (V) = Last_Index (V)'Loop_Entry);
16 pragma Loop_Invariant
17 (for all I in 1 .. Last_Index (V) =>
18 (if I in First .. J then Element (V, I) = 0
19 else Element (V, I) = Element (Model (V)'Loop_Entry, I)));
20 end loop;
21end 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 preservation proved
update_range_vec_zero.adb:15:30: info: loop invariant initialization proved
update_range_vec_zero.adb:17:10: info: loop invariant preservation proved
update_range_vec_zero.adb:17:10: info: loop invariant initialization 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:
1with Loop_Types; use Loop_Types; use Loop_Types.Lists;
2with Ada.Containers; use Ada.Containers; use Loop_Types.Lists.Formal_Model;
3
4procedure Update_Range_List_Zero (L : in out List_T; First, Last : Cursor) with
5 SPARK_Mode,
6 Pre => Has_Element (L, First) and then Has_Element (L, Last)
7 and then P.Get (Positions (L), First) <= P.Get (Positions (L), Last),
8 Post => Length (L) = Length (L)'Old
9 and Positions (L) = Positions (L)'Old
10 and (for all I in 1 .. Length (L) =>
11 (if I in P.Get (Positions (L), First) .. P.Get (Positions (L), Last) then
12 Element (Model (L), I) = 0
13 else Element (Model (L), I) = Element (Model (L'Old), I)))
14is
15 Cu : Cursor := First;
16begin
17 loop
18 pragma Loop_Invariant (Has_Element (L, Cu));
19 pragma Loop_Invariant (P.Get (Positions (L), Cu) in P.Get (Positions (L), First) .. P.Get (Positions (L), Last));
20 pragma Loop_Invariant (Length (L) = Length (L)'Loop_Entry);
21 pragma Loop_Invariant (Positions (L) = Positions (L)'Loop_Entry);
22 pragma Loop_Invariant (for all I in 1 .. Length (L) =>
23 (if I in P.Get (Positions (L), First) .. P.Get (Positions (L), Cu) - 1 then
24 Element (Model (L), I) = 0
25 else Element (Model (L), I) = Element (Model (L'Loop_Entry), I)));
26 Replace_Element (L, Cu, 0);
27 exit when Cu = Last;
28 Next (L, Cu);
29 end loop;
30end 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:19:30: info: loop invariant preservation proved
update_range_list_zero.adb:19:30: info: loop invariant initialization proved
update_range_list_zero.adb:19:31: info: precondition 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 preservation proved
update_range_list_zero.adb:20:30: info: loop invariant initialization proved
update_range_list_zero.adb:21:30: info: loop invariant preservation proved
update_range_list_zero.adb:21:30: info: loop invariant initialization proved
update_range_list_zero.adb:22:30: info: loop invariant preservation proved
update_range_list_zero.adb:22:30: info: loop invariant initialization 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: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:28:07: info: precondition proved