5.6. Assertion Pragmas
SPARK contains features for directing formal verification with
GNATprove. These features may also be used by other tools, in particular the
GNAT compiler. Assertion pragmas are refinements of pragma Assert
defined in Ada. For all assertion pragmas, an exception Assertion_Error
is
raised at run time when the property asserted does not hold, if the program was
compiled with assertions. The real difference between assertion pragmas is how
they are used by GNATprove during proof.
5.6.1. Pragma Assert
[Ada 2005]
Pragma Assert
is the simplest assertion pragma. GNATprove checks that the
property asserted holds, and uses the information that it holds for analyzing
code that follows. For example, consider two assertions of the same property
X > 0
in procedure Assert_Twice
:
1procedure Assert_Twice (X : Integer) with
2 SPARK_Mode
3is
4begin
5 pragma Assert (X > 0);
6 pragma Assert (X > 0);
7end Assert_Twice;
As expected, the first assertion on line 5 is not provable in absence of a
suitable precondition for Assert_Twice
, but GNATprove proves that it
holds the second time the property is asserted on line 6:
assert_twice.adb:5:19: high: assertion might fail
5 | pragma Assert (X > 0);
| ^~~~~
e.g. when X = 0
possible fix: subprogram at line 1 should mention X in a precondition
1 |procedure Assert_Twice (X : Integer) with
|^ here
assert_twice.adb:6:19: info: assertion proved
GNATprove considers that an execution of Assert_Twice
with X <= 0
stops at the first assertion that fails. Thus X > 0
when execution reaches
the second assertion. This is true if assertions are executed at run time, but
not if assertions are discarded during compilation. In the latter case,
unproved assertions should be inspected carefully to ensure that the property
asserted will indeed hold at run time. This is true of all assertion pragmas,
which GNATprove analyzes like pragma Assert
in that respect.
5.6.2. Pragma Assertion_Policy
[Ada 2005/Ada 2012]
Assertions can be enabled either globally or locally. Here, assertions denote either Assertion Pragmas of all kinds (among which Pragma Assert) or functional contracts of all kinds (among which Preconditions and Postconditions).
By default, assertions are ignored in compilation, and can be enabled globally
by using the compilation switch -gnata
. They can be enabled locally by
using pragma Assertion_Policy
in the program, or globally if the pragma is
put in a configuration file. They can be enabled for all kinds of assertions or
specific ones only by using the version of pragma Assertion_Policy
that
takes named associations which was introduced in Ada 2012.
When used with the standard policies Check
(for enabling assertions) or
Ignore
(for ignoring assertions), pragma Assertion_Policy
has no
effect on GNATprove. GNATprove takes all assertions into account, whatever
the assertion policy in effect at the point of the assertion. For example,
consider a code with some assertions enabled and some ignored:
1pragma Assertion_Policy (Pre => Check, Post => Ignore);
2
3procedure Assert_Enabled (X : in out Integer) with
4 SPARK_Mode,
5 Pre => X > 0, -- executed at run time
6 Post => X > 2 -- ignored at run time
7is
8 pragma Assertion_Policy (Assert => Check);
9 pragma Assert (X >= 0); -- executed at run time
10
11 pragma Assertion_Policy (Assert => Ignore);
12 pragma Assert (X >= 0); -- ignored at run time
13begin
14 X := X - 1;
15end Assert_Enabled;
Although the postcondition and the second assertion are not executed at run time, GNATprove analyzes them and issues corresponding messages:
assert_enabled.adb:6:11: high: postcondition might fail
6 | Post => X > 2 -- ignored at run time
| ^~~~~
e.g. when X = 0
assert_enabled.adb:9:19: info: assertion proved
assert_enabled.adb:12:19: info: assertion proved
assert_enabled.adb:14:11: info: overflow check proved
On the contrary, when used with the GNAT-specific policy Disable
, pragma
Assertion_Policy
causes the corresponding assertions to be skipped both
during execution and analysis with GNATprove. For example, consider the same
code as above where policy Ignore
is replaced with policy Disable
:
1pragma Assertion_Policy (Pre => Check, Post => Disable);
2
3procedure Assert_Disabled (X : in out Integer) with
4 SPARK_Mode,
5 Pre => X > 0, -- executed at run time
6 Post => X > 2 -- ignored at compile time and in analysis
7is
8 pragma Assertion_Policy (Assert => Check);
9 pragma Assert (X >= 0); -- executed at run time
10
11 pragma Assertion_Policy (Assert => Disable);
12 pragma Assert (X >= 0); -- ignored at compile time and in analysis
13begin
14 X := X - 1;
15end Assert_Disabled;
On this program, GNATprove does not analyze the postcondition and the second assertion, and it does not issue corresponding messages:
assert_disabled.adb:9:19: info: assertion proved
assert_disabled.adb:14:11: info: overflow check proved
The policy of Disable
should thus be reserved for assertions that are not
compilable, typically because a given build environment does not define the
necessary entities.
5.6.3. Loop Invariants
[SPARK]
Pragma Loop_Invariant
is a special kind of assertion used in
loops. GNATprove performs two checks that ensure that the property asserted
holds at each iteration of the loop:
loop invariant initialization: GNATprove checks that the property asserted holds during the first iteration of the loop.
loop invariant preservation: GNATprove checks that the property asserted holds during an arbitrary iteration of the loop, assuming that it held in the previous iteration.
Each of these properties can be independently true or false. For example, in the following loop, the loop invariant is false during the first iteration and true in all remaining iterations:
6 Prop := False;
7 for J in 1 .. 10 loop
8 pragma Loop_Invariant (Prop);
9 Prop := True;
10 end loop;
Thus, GNATprove checks that property 2 holds but not property 1:
simple_loops.adb:8:30: high: loop invariant might fail in first iteration
8 | pragma Loop_Invariant (Prop);
| ^~~~
e.g. when Prop = False
simple_loops.adb:8:30: info: loop invariant preservation proved
Conversely, in the following loop, the loop invariant is true during the first iteration and false in all remaining iterations:
12 Prop := True;
13 for J in 1 .. 10 loop
14 pragma Loop_Invariant (Prop);
15 Prop := False;
16 end loop;
Thus, GNATprove checks that property 1 holds but not property 2:
simple_loops.adb:14:30: info: loop invariant initialization proved
simple_loops.adb:14:30: medium: loop invariant might not be preserved by an arbitrary iteration
14 | pragma Loop_Invariant (Prop);
| ^~~~
The following loop shows a case where the loop invariant holds both during the first iteration and all remaining iterations:
18 Prop := True;
19 for J in 1 .. 10 loop
20 pragma Loop_Invariant (Prop);
21 Prop := Prop;
22 end loop;
GNATprove checks here that both properties 1 and 2 hold:
simple_loops.adb:20:30: info: loop invariant preservation proved
simple_loops.adb:20:30: info: loop invariant initialization proved
In general, it is not sufficient that a loop invariant is true for GNATprove to prove it. The loop invariant should also be inductive: it should be precise enough that GNATprove can check loop invariant preservation by assuming only that the loop invariant held during the last iteration. For example, the following loop is the same as the previous one, except the loop invariant is true but not inductive:
24 Prop := True;
25 for J in 1 .. 10 loop
26 pragma Loop_Invariant (if J > 1 then Prop);
27 Prop := Prop;
28 end loop;
GNATprove cannot check property 2 on that loop:
simple_loops.adb:26:30: info: loop invariant initialization proved
simple_loops.adb:26:44: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Prop
26 | pragma Loop_Invariant (if J > 1 then Prop);
| ^~~~
Note also that not using an assertion (Pragma Assert) instead of a loop invariant also allows here to fully prove the corresponding property, by relying on Automatic Unrolling of Simple For-Loops:
simple_loops_unroll.adb:26:22: info: assertion proved
Returning to the case where automatic loop unrolling is not used, the reasoning of GNATprove for checking property 2 in that case can be summarized as follows:
Let’s take iteration K of the loop, where K > 1 (not the first iteration).
Let’s assume that the loop invariant held during iteration K-1, so we know that if K-1 > 1 then Prop holds.
The previous assumption can be rewritten: if K > 2 then Prop.
But all we know is that K > 1, so we cannot deduce Prop.
See How to Write Loop Invariants for further guidelines.
Pragma Loop_Invariant
may appear anywhere at the top level of a loop: it is
usually added at the start of the loop, but it may be more convenient in some
cases to add it at the end of the loop, or in the middle of the loop, in cases
where this simplifies the asserted property. In all cases, GNATprove checks
loop invariant preservation by reasoning on the virtual loop that starts and
ends at the loop invariant.
It is possible to use multiple loop invariants, which should be grouped
together without intervening statements, declarations or pragmas, at the
exception of pragma Loop_Variant
and pragma Annotate
(to justify check
messages). The resulting complete loop invariant is the conjunction of
individual ones. The benefits of writing multiple loop invariants instead of a
conjunction can be improved readability and better provability (because
GNATprove checks each pragma Loop_Invariant
separately).
Finally, Attribute Loop_Entry and Delta Aggregates can be very useful to express complex loop invariants.
Note
Users that are already familiar with the notion of loop invariant in other proof systems should be aware that loop invariants in SPARK are slightly different from the usual ones. In SPARK, a loop invariant must hold when execution reaches the corresponding pragma inside the loop. Hence, it needs not hold when the loop is never entered, or when exiting the loop.
5.6.4. Loop Variants
[SPARK]
Pragma Loop_Variant
is a special kind of assertion used in
loops. GNATprove checks that the given value progresses in some sense at
each iteration of
the loop. The value is associated to a direction, which can be either
Increases
or Decreases
for numeric variants, or Structural
for
structural variants.
Numeric variants can take a discrete value or, in the
case of the direction Decreases
, a big natural (see
SPARK.Big_Integers
). At each iteration, a check is generated
to ensure that the value progresses (decreases or increases) with respect to its
value at the beginning of the loop. Because a discrete value is always bounded
by its type in Ada, and a big natural is never negative, it cannot decrease (or
increase) at each iteration an infinite number of times, thus one of two
outcomes is possible:
the loop exits, or
a run-time error occurs.
Therefore, it is possible to prove the termination of loops in SPARK programs by proving both a loop variant for each plain-loop or while-loop (for-loops always terminate in Ada) and the absence of run-time errors.
For example, the while-loops in procedure Terminating_Loops
compute the
value of X - X mod 3
(or equivalently X / 3 * 3
) in variable Y
:
1procedure Terminating_Loops (X : Natural) with
2 SPARK_Mode
3is
4 Y : Natural;
5begin
6 Y := 0;
7 while X - Y >= 3 loop
8 Y := Y + 3;
9 pragma Loop_Variant (Increases => Y);
10 end loop;
11
12 Y := 0;
13 while X - Y >= 3 loop
14 Y := Y + 3;
15 pragma Loop_Variant (Decreases => X - Y);
16 end loop;
17end Terminating_Loops;
GNATprove is able to prove both loop variants, as well as absence of run-time errors in the subprogram, hence that loops terminate:
terminating_loops.adb:4:04: info: initialization of "Y" proved
terminating_loops.adb:7:12: info: overflow check proved
terminating_loops.adb:8:14: info: overflow check proved
terminating_loops.adb:9:28: info: loop variant proved
terminating_loops.adb:13:12: info: overflow check proved
terminating_loops.adb:14:14: info: overflow check proved
terminating_loops.adb:15:28: info: loop variant proved
terminating_loops.adb:15:43: info: overflow check proved
A numeric loop variant may be more complex than a single decreasing (or increasing) value, and be given instead by a list of either decreasing or increasing values (possibly a mix of both). In that case, the order of the list defines the lexicographic order of progress. See SPARK RM 5.5.3 for details.
The expression of a structural loop variant can be either a local borrower or a local observer (see Observing and Borrowing). A check is generated to ensure that, during each iteration of the loop, the object denoted by the variant is updated to designate a strict subcomponent of the structure it used to designate. Since, due to the Memory Ownership Policy of SPARK, the structure cannot contain cycles, it is enough to ensure that the loop cannot be executed an infinite number of times.
In the following example, we can verify that the while
loop in the
Set_All_To_Zero
procedure terminates by stating that the local borrower
X
used to traverse the linked list structurally decreases at each iteration:
1package Terminating_Loops with
2 SPARK_Mode
3is
4 type Cell;
5 type List is access Cell;
6 type Cell is record
7 Value : Integer;
8 Next : List;
9 end record;
10
11 procedure Set_All_To_Zero (L : List);
12
13end Terminating_Loops;
1package body Terminating_Loops with
2 SPARK_Mode
3is
4
5 procedure Set_All_To_Zero (L : List) is
6 X : access Cell := L;
7 begin
8 while X /= null loop
9 pragma Loop_Variant (Structural => X);
10 X.Value := 0;
11 X := X.Next;
12 end loop;
13 end Set_All_To_Zero;
14
15end Terminating_Loops;
Structural variants are subjects to a number of restrictions.
They cannot be combined with other variants, and are checked according to
a mostly syntactic criterion. When these restrictions cannot be followed,
structural variants can be systematically replaced by a decreasing numeric
variant providing the depth (or size) of the data structure, like function
Length
in Subprogram Variant. Strictly speaking, structural variants are only required
to define the function returning that metric.
The fact that, at each iteration, the variable X
is updated to designate a
strict subcomponent of the structure it used to designate can
be verified by GNATprove:
terminating_loops.adb:9:10: info: loop variant proved
terminating_loops.adb:10:11: info: pointer dereference check proved
terminating_loops.adb:11:16: info: pointer dereference check proved
Pragma Loop_Variant
may appear anywhere a loop invariant appears. It is
also possible to use multiple loop variants, which should be grouped together
with loop invariants.
5.6.5. Pragma Assume
[SPARK]
Pragma Assume
is a variant of Pragma Assert that does not require
GNATprove to check that the property holds. This is used to convey trustable
information to GNATprove, in particular properties about external objects
that GNATprove has no control upon. GNATprove uses the information that the
assumed property holds for analyzing code that follows. For example, consider
an assumption of the property X > 0
in procedure Assume_Then_Assert
,
followed by an assertion of the same property:
1procedure Assume_Then_Assert (X : Integer) with
2 SPARK_Mode
3is
4begin
5 pragma Assume (X > 0);
6 pragma Assert (X > 0);
7end Assume_Then_Assert;
As expected, GNATprove does not check the property on line 5, but used it to prove that the assertion holds on line 6:
assume_then_assert.adb:6:19: info: assertion proved
GNATprove considers that an execution of Assume_Then_Assert
with X <=
0
stops at the assumption on line 5, and it does not issue a message in that
case because the user explicitly indicated that this case is not possible. Thus
X > 0
when execution reaches the assertion on line 6. This is true if
assertions (of which assumptions are a special kind) are executed at run time,
but not if assertions are discarded during compilation. In the latter case,
assumptions should be inspected carefully to ensure that the property assumed
will indeed hold at run time. This inspection may be facilitated by passing a
justification string as the second argument to pragma Assume
.
5.6.6. Pragma Assert_And_Cut
[SPARK]
Pragma Assert_And_Cut
is a variant of Pragma Assert that allows
hiding some information to GNATprove. GNATprove checks that the property
asserted holds, and uses only the information that it holds for analyzing
code that follows. For example, consider two assertions of the same property
X = 1
in procedure Forgetful_Assert
, separated by a pragma
Assert_And_Cut
:
1procedure Forgetful_Assert (X : out Integer) with
2 SPARK_Mode
3is
4begin
5 X := 1;
6
7 pragma Assert (X = 1);
8
9 pragma Assert_And_Cut (X > 0);
10
11 pragma Assert (X > 0);
12 pragma Assert (X = 1);
13end Forgetful_Assert;
GNATprove proves that the assertion on line 7 holds, but it cannot prove that the same assertion on line 12 holds:
forgetful_assert.adb:1:29: info: initialization of "X" proved
forgetful_assert.adb:7:19: info: assertion proved
forgetful_assert.adb:9:27: info: assertion proved
forgetful_assert.adb:11:19: info: assertion proved
forgetful_assert.adb:12:19: medium: assertion might fail
12 | pragma Assert (X = 1);
| ^~~~~
GNATprove forgets the exact value of X
after line 9. All it knows is
the information given in pragma Assert_And_Cut
, here that X > 0
. And
indeed GNATprove proves that such an assertion holds on line 11. But it
cannot prove the assertion on line 12, showing indeed that GNATprove
forgot its value of 1.
Pragma Assert_And_Cut
may be useful in two cases:
When the automatic provers are overwhelmed with information from the context, pragma
Assert_And_Cut
may be used to simplify this context, thus leading to more automatic proofs.When GNATprove is proving checks for each path through the subprogram (see switch
--proof
in Running GNATprove from the Command Line), and the number of paths is very large, pragmaAssert_And_Cut
may be used to reduce the number of paths, thus leading to faster automatic proofs.For example, consider procedure
P
below, where all that is needed to prove that the code usingX
is free from run-time errors is thatX
is positive. Let’s assume that we are running GNATprove with switch--proof=per_path
so that a formula is generated for each execution path. Without the pragma, GNATprove considers all execution paths throughP
, which may be many. With the pragma, GNATprove only considers the paths from the start of the procedure to the pragma, and the paths from the pragma to the end of the procedure, hence many fewer paths.
1procedure P is
2 X : Integer;
3begin
4 -- complex computation that sets X
5 pragma Assert_And_Cut (X > 0);
6 -- complex computation that uses X
7end P;
GNATprove only forgets information from inside the enclosing sequence of statements, meaning information about
variables modified since the start of the enclosing sequence of statements
Boolean tests (including checks) that must have evaluated to true for control to reach the pragma from the start of the enclosing sequence of statements.
Procedure Partial_Knowledge
below shows examples of informations
that are remembered and forgotten.
1procedure Partial_Knowledge (X : Integer) is
2 Y : Integer;
3 Z : Integer;
4begin
5 Y := 0;
6 if (X <= 0) then
7 return;
8 end if;
9 begin
10 Z := 1;
11 begin
12 if (X >= 2) then
13 return;
14 end if;
15 end;
16 pragma Assert_And_Cut (Y < Z);
17 pragma Assert (Y = 0); -- Remembered
18 pragma Assert (X > 0); -- Remembered
19 pragma Assert (Y < Z); -- From cut
20 pragma Assert (Z = 1); -- Forgotten
21 pragma Assert (X < 2); -- Forgotten
22 end;
23end;
Since variable Y
is not modified in the inner block, the information
that Y
was zero is not forgotten, and the assertion at line 17 is proved.
Similarly, GNATprove does not forget that X
must have been positive
to reach the inner block in the first place, and proves the assertion at line 18.
However, it does not prove the following assertions at lines 20/21, and displays
counter-examples with values of 2 for X,Z
, showing indeed
that GNATprove forgot the value of Z
, as well as the fact that
the program should have exited already when X
is 2.
partial_knowledge.adb:2:04: info: initialization of "Y" proved
partial_knowledge.adb:3:04: info: initialization of "Z" proved
partial_knowledge.adb:16:30: info: assertion proved
partial_knowledge.adb:17:22: info: assertion proved
partial_knowledge.adb:18:22: info: assertion proved
partial_knowledge.adb:19:22: info: assertion proved
partial_knowledge.adb:20:22: medium: assertion might fail
20 | pragma Assert (Z = 1); -- Forgotten
| ^~~~~
e.g. when Z = 2
possible fix: add or complete related loop invariants or postconditions
partial_knowledge.adb:21:22: medium: assertion might fail
21 | pragma Assert (X < 2); -- Forgotten
| ^~~~~
e.g. when X = 2
possible fix: subprogram at line 1 should mention X in a precondition
1 |procedure Partial_Knowledge (X : Integer) is
|^ here
Note
Due to pragmas Assert_And_Cut
and Loop_Invariant
both acting as
cut points for verification, but in slightly different ways, GNATprove
does not support the full breadth of their potential interactions.
Pragma Assert_And_Cut
is only supported within loops when the
immediately surrounding statement sequence does not contain the
loop invariants, including any occurring within nested blocks.
GNATprove also supports as a convenience the special case when the
loop invariants occurs at top level in the sequence prefix
preceding pragma Assert_And_Cut
, by implicitly assuming that a
new block starts immediately after the last pragma Loop_Invariant
.