7.4. How to Write Subprogram Contracts
GNATprove relies on contracts to perform its analysis. User-specified subprogram contracts are assumed to analyze a subprogram’s callers, and verified when the body of the subprogram is analyzed.
By default, no contracts are compulsory in GNATprove. In the absence of user-provided contracts, GNATprove internally generates default contracts, which may or not be suitable depending on the verification objective:
data dependencies (
Global
)See Generation of Dependency Contracts. The generated contract may be exact when completed from user-specified flow dependencies (Depends), or precise when generated from a body in SPARK, or coarse when generated from a body in full Ada.
flow dependencies (
Depends
)See Generation of Dependency Contracts. The contract is generated from the user-specified or generated data dependencies, by considering that all outputs depend on all inputs.
precondition (
Pre
)A default precondition of
True
is used in absence of a user-specified precondition.postcondition (
Post
)A default postcondition of
True
is used in absence of a user-specified postcondition, except for expression functions. For the latter, the body of the expression function is used to generate a matching postcondition. See Expression Functions.exceptional contract (
Exceptional_Cases
)As a default, procedures are not considered to raise any exceptions (
Exceptional_Cases => (others => False)
).termination contract (
Always_Terminates
)The contract is generated from a body in SPARK and a default contract of
False
is used if the body is in full Ada. If there is no body, a default contract ofTrue
(orFalse
for No_Return procedures) is used.
Knowing which contracts to write depends on the specific verification objectives to achieve.
7.4.1. Generation of Dependency Contracts
By default, GNATprove does not require the user to write data dependencies
(introduced with aspect Global
) and flow dependencies (introduced
with aspect Depends
), as it can automatically generate them from the
program.
This behavior can be disabled using the --no-global-generation
switch,
which means a missing data dependency is the same as Global => null
.
Note that this option also forces --no-inlining
(see Contextual Analysis of Subprograms Without Contracts).
Note
GNATprove does not generate warning or check messages when the body of a subprogram does not respect a generated contract. Indeed, the generated contract is a safe over-approximation of the real contract, hence it is unlikely that the subprogram body respects it. The generated contract is used instead to verify proper initialization and respect of dependency contracts in the callers of the subprogram.
Note
Intrinsic subprograms such as arithmetic operations, and shift/rotate functions without user-provided functional contracts (precondition, postcondition or contract cases) are handled specially by GNATprove.
Note
The --no-global-generation
switch makes GNATprove behave more like
the previous SPARK 2005 tools, which makes this switch attractive
for project trying to migrate to the new GNATprove tools, or for
projects that maintain dual annotations.
7.4.1.1. Auto Completion for Incomplete Contracts
When only the data dependencies (resp. only the flow dependencies) are given on a subprogram, GNATprove completes automatically the subprogram contract with the matching flow dependencies (resp. data dependencies).
Writing Only the Data Dependencies
When only the data dependencies are given on a subprogram, GNATprove completes them with flow dependencies that have all outputs depending on all inputs. This is a safe over-approximation of the real contract of the subprogram, which allows to detect all possible errors of initialization and contract violation in the subprogram and its callers, but which may also lead to false alarms because it is imprecise.
Take for example procedures Add
and Swap
for which data dependencies
are given, but no flow dependencies:
1package Only_Data_Dependencies with
2 SPARK_Mode
3is
4 V : Integer;
5
6 procedure Add (X : Integer) with
7 Global => (In_Out => V);
8
9 procedure Swap (X : in out Integer) with
10 Global => (In_Out => V);
11
12 procedure Call_Add (X, Y : Integer) with
13 Global => (In_Out => V),
14 Depends => (V =>+ (X, Y));
15
16 procedure Call_Swap (X, Y : in out Integer) with
17 Global => (In_Out => V),
18 Depends => (X => Y, Y => X, V => V);
19
20end Only_Data_Dependencies;
GNATprove completes the contract of Add
and Swap
with flow
dependencies that are equivalent to:
procedure Add (X : Integer) with
Global => (In_Out => V),
Depends => (V =>+ X);
procedure Swap (X : in out Integer) with
Global => (In_Out => V),
Depends => ((X, V) => (X, V));
Other flow dependencies with fewer dependencies between inputs and outputs
would be compatible with the given data dependencies of Add
and
Swap
. GNATprove chooses the contracts with the most dependencies. Here,
this corresponds to the actual contract for Add
, but to an imprecise
contract for Swap
:
1package body Only_Data_Dependencies with
2 SPARK_Mode
3is
4 procedure Add (X : Integer) is
5 begin
6 V := V + X;
7 end Add;
8
9 procedure Swap (X : in out Integer) is
10 Tmp : constant Integer := V;
11 begin
12 V := X;
13 X := Tmp;
14 end Swap;
15
16 procedure Call_Add (X, Y : Integer) is
17 begin
18 Add (X);
19 Add (Y);
20 end Call_Add;
21
22 procedure Call_Swap (X, Y : in out Integer) is
23 begin
24 Swap (X);
25 Swap (Y);
26 Swap (X);
27 end Call_Swap;
28
29end Only_Data_Dependencies;
This results in false alarms when GNATprove verifies the dependency contract
of procedure Call_Swap
which calls Swap
, while it succeeds in verifying
the dependency contract of Call_Add
which calls Add
:
only_data_dependencies.adb:6:14: high: overflow check might fail, cannot prove lower bound for V + X
6 | V := V + X;
| ~~^~~
e.g. when V = Integer'First
and X = -1
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: subprogram at only_data_dependencies.ads:6 should mention X and V in a precondition
6 | procedure Add (X : Integer) with
| ^ here
only_data_dependencies.ads:18:18: medium: missing dependency "X => V"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
only_data_dependencies.ads:18:18: medium: missing self-dependency "X => X"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
only_data_dependencies.ads:18:26: medium: missing dependency "Y => V"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
only_data_dependencies.ads:18:26: medium: missing self-dependency "Y => Y"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
only_data_dependencies.ads:18:34: medium: missing dependency "V => X"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
only_data_dependencies.ads:18:34: medium: missing dependency "V => Y"
18 | Depends => (X => Y, Y => X, V => V);
| ^ here
The most precise dependency contract for Swap
would be:
procedure Swap (X : in out Integer) with
Global => (In_Out => V),
Depends => (V => X, X => V);
If you add this precise contract in the program, then GNATprove can also
verify the dependency contract of Call_Swap
.
Note that the generated dependency contracts are used in the analysis of
callers, but GNATprove generates no warnings or check messages if the body of
Add
or Swap
have fewer flow dependencies, as seen above. That’s a
difference between these contracts being present in the code or auto completed.
Writing Only the Flow Dependencies
When only the flow dependencies are given on a subprogram, GNATprove completes it with the only compatible data dependencies.
Take for example procedures Add
and Swap
as previously, expect now flow
dependencies are given, but no data dependencies:
1package Only_Flow_Dependencies with
2 SPARK_Mode
3is
4 V : Integer;
5
6 procedure Add (X : Integer) with
7 Depends => (V =>+ X);
8
9 procedure Swap (X : in out Integer) with
10 Depends => (V => X, X => V);
11
12 procedure Call_Add (X, Y : Integer) with
13 Global => (In_Out => V),
14 Depends => (V =>+ (X, Y));
15
16 procedure Call_Swap (X, Y : in out Integer) with
17 Global => (In_Out => V),
18 Depends => (X => Y, Y => X, V => V);
19
20end Only_Flow_Dependencies;
The body of the unit is the same as before:
1package body Only_Flow_Dependencies with
2 SPARK_Mode
3is
4 procedure Add (X : Integer) is
5 begin
6 V := V + X;
7 end Add;
8
9 procedure Swap (X : in out Integer) is
10 Tmp : constant Integer := V;
11 begin
12 V := X;
13 X := Tmp;
14 end Swap;
15
16 procedure Call_Add (X, Y : Integer) is
17 begin
18 Add (X);
19 Add (Y);
20 end Call_Add;
21
22 procedure Call_Swap (X, Y : in out Integer) is
23 begin
24 Swap (X);
25 Swap (Y);
26 Swap (X);
27 end Call_Swap;
28
29end Only_Flow_Dependencies;
GNATprove verifies the data and flow dependencies of all
subprograms, including Call_Add
and Call_Swap
, based on the completed
contracts for Add
and Swap
.
7.4.1.2. Precise Generation for SPARK Subprograms
When no data or flow dependencies are given on a SPARK subprogram, GNATprove generates precise data and flow dependencies by using path-sensitive flow analysis to track data flows in the subprogram body:
if a variable is written completely on all paths in a subprogram body, it is considered an output of the subprogram; and
other variables that are written in a subprogram body are considered both inputs and outputs of the subprogram (even if they are not read explicitly, their output value may depend on their input value); and
if a variable is only read in a subprogram body, it is considered an input of the subprogram; and
all outputs are considered to potentially depend on all inputs.
Case 1: No State Abstraction
Take for example a procedure Set_Global
without contract which initializes
a global variable V
and is called in a number of contexts:
1package Gen_Global with
2 SPARK_Mode
3is
4 procedure Set_Global;
5
6 procedure Do_Nothing;
7
8 procedure Set_Global_Twice;
9
10end Gen_Global;
1package body Gen_Global with
2 SPARK_Mode
3is
4 V : Boolean;
5
6 procedure Set_Global is
7 begin
8 V := True;
9 end Set_Global;
10
11 procedure Do_Nothing is
12 begin
13 null;
14 end Do_Nothing;
15
16 procedure Set_Global_Twice is
17 begin
18 Set_Global;
19 Set_Global;
20 end Set_Global_Twice;
21
22 procedure Set_Global_Conditionally (X : Boolean) with
23 Global => (Output => V),
24 Depends => (V => X)
25 is
26 begin
27 if X then
28 Set_Global;
29 else
30 V := False;
31 end if;
32 end Set_Global_Conditionally;
33
34end Gen_Global;
GNATprove generates data and flow dependencies for procedure
Set_Global
that are equivalent to:
procedure Set_Global with
Global => (Output => V),
Depends => (V => null);
Note that the above contract would be illegal as given, because it refers to
global variable V
which is not visible at the point where Set_Global
is
declared in gen_global.ads
. Instead, a user who would like to write this
contract on Set_Global
would have to use abstract state.
That generated contract for Set_Global
allows GNATprove to both detect
possible errors when calling Set_Global
and to verify contracts given by
the user on callers of Set_Global
. For example, procedure
Set_Global_Twice
calls Set_Global
twice in a row, which makes the first
call useless as the value written in V
is immediately overwritten by the
second call. This is detected by GNATprove, which issues two warnings on
line 18:
gen_global.adb:18:07: warning: statement has no effect
18 | Set_Global;
| ^~~~~~~~~~
gen_global.adb:18:07: warning: "V" is set by "Set_Global" but not used after the call
18 | Set_Global;
| ^~~~~~~~~~
GNATprove also uses the generated contract for Set_Global
to analyze
procedure Set_Global_Conditionally
, which allows it to verify the contract
given by the user for Set_Global_Conditionally
:
procedure Set_Global_Conditionally (X : Boolean) with
Global => (Output => V),
Depends => (V => X)
Case 2: State Abstraction Without Dependencies
If an abstract state (see State Abstraction) is declared by the user but no dependencies are specified on subprogram declarations, then GNATprove generates data and flow dependencies which take abstract state into account.
For example, take unit Gen_Global
previously seen, where an abstract state
State
is defined for package Gen_Abstract_Global
, and refined into
global variable V
in the body of the package:
1package Gen_Abstract_Global with
2 SPARK_Mode,
3 Abstract_State => State
4is
5 procedure Set_Global;
6
7 procedure Set_Global_Twice;
8
9 procedure Set_Global_Conditionally (X : Boolean) with
10 Global => (Output => State),
11 Depends => (State => X);
12
13end Gen_Abstract_Global;
1package body Gen_Abstract_Global with
2 SPARK_Mode,
3 Refined_State => (State => V)
4is
5 V : Boolean;
6
7 procedure Set_Global is
8 begin
9 V := True;
10 end Set_Global;
11
12 procedure Set_Global_Twice is
13 begin
14 Set_Global;
15 Set_Global;
16 end Set_Global_Twice;
17
18 procedure Set_Global_Conditionally (X : Boolean) with
19 Refined_Global => (Output => V),
20 Refined_Depends => (V => X)
21 is
22 begin
23 if X then
24 Set_Global;
25 else
26 V := False;
27 end if;
28 end Set_Global_Conditionally;
29
30end Gen_Abstract_Global;
We have chosen here to declare procedure Set_Global_Conditionally
in
gen_abstract_global.ads
, and so to express its user contract abstractly. We
could also have kept it local to the unit.
GNATprove gives the same results on this unit as before: it issues warnings
for the possible error in Set_Global_Twice
and it verifies the contract
given by the user for Set_Global_Conditionally
:
gen_abstract_global.adb:14:07: warning: statement has no effect
14 | Set_Global;
| ^~~~~~~~~~
gen_abstract_global.adb:14:07: warning: "V" constituent of "State" is set by "Set_Global" but not used after the call
14 | Set_Global;
| ^~~~~~~~~~
Case 3: State Abstraction Without Refined Dependencies
If abstract state is declared by the user and abstract dependencies are specified on subprogram declarations, but no refined dependencies are specified on subprogram implementations (as described State Abstraction and Dependencies), then GNATprove generates refined data and flow dependencies for subprogram implementations.
For example, take unit Gen_Abstract_Global
previously seen, where only
abstract data and flow dependencies are specified:
1package Gen_Refined_Global with
2 SPARK_Mode,
3 Abstract_State => State
4is
5 procedure Set_Global with
6 Global => (Output => State);
7
8 procedure Set_Global_Twice with
9 Global => (Output => State);
10
11 procedure Set_Global_Conditionally (X : Boolean) with
12 Global => (Output => State),
13 Depends => (State => X);
14
15end Gen_Refined_Global;
1package body Gen_Refined_Global with
2 SPARK_Mode,
3 Refined_State => (State => V)
4is
5 V : Boolean;
6
7 procedure Set_Global is
8 begin
9 V := True;
10 end Set_Global;
11
12 procedure Set_Global_Twice is
13 begin
14 Set_Global;
15 Set_Global;
16 end Set_Global_Twice;
17
18 procedure Set_Global_Conditionally (X : Boolean) is
19 begin
20 if X then
21 Set_Global;
22 else
23 Set_Global;
24 end if;
25 end Set_Global_Conditionally;
26
27end Gen_Refined_Global;
GNATprove gives the same results on this unit as before: it issues warnings
for the possible error in Set_Global_Twice
and it verifies the contract
given by the user for Set_Global_Conditionally
:
gen_refined_global.adb:14:07: warning: statement has no effect
14 | Set_Global;
| ^~~~~~~~~~
gen_refined_global.adb:14:07: warning: "V" constituent of "State" is set by "Set_Global" but not used after the call
14 | Set_Global;
| ^~~~~~~~~~
Note that although abstract and refined dependencies are the same here, this is not always the case, and GNATprove will use the more precise generated dependencies to analyze calls to subprograms inside the unit.
7.4.1.3. Coarse Generation for non-SPARK Subprograms
When no data or flow dependencies are given on a non-SPARK subprogram, GNATprove generates coarser data and flow dependencies based on the reads and writes to variables in the subprogram body:
if a variable is written in a subprogram body, it is considered both an input and an output of the subprogram; and
if a variable is only read in a subprogram body, it is considered an input of the subprogram; and
all outputs are considered to potentially depend on all inputs.
For example, take unit Gen_Global
previously seen, where the body of
Set_Global
is marked with SPARK_Mode => Off
:
1package Gen_Ada_Global with
2 SPARK_Mode
3is
4 procedure Set_Global;
5
6 procedure Set_Global_Twice;
7
8end Gen_Ada_Global;
1package body Gen_Ada_Global with
2 SPARK_Mode
3is
4 V : Boolean;
5
6 procedure Set_Global with
7 SPARK_Mode => Off
8 is
9 begin
10 V := True;
11 end Set_Global;
12
13 procedure Set_Global_Twice is
14 begin
15 Set_Global;
16 Set_Global;
17 end Set_Global_Twice;
18
19 procedure Set_Global_Conditionally (X : Boolean) with
20 Global => (Output => V),
21 Depends => (V => X)
22 is
23 begin
24 if X then
25 Set_Global;
26 else
27 V := False;
28 end if;
29 end Set_Global_Conditionally;
30
31end Gen_Ada_Global;
GNATprove generates a data and flow dependencies for procedure
Set_Global
that are equivalent to:
procedure Set_Global with
Global => (In_Out => V),
Depends => (V => V);
This is a safe over-approximation of the real contract for
Set_Global
, which allows to detect all possible errors of initialization
and contract violation in Set_Global
callers, but which may also lead to
false alarms because it is imprecise. Here, GNATprove generates a wrong
high message that the call to Set_Global
on line 25 reads an uninitialized value
for V
:
gen_ada_global.adb:25:10: high: "V" is not an input in the Global contract of subprogram "Set_Global_Conditionally" at line 19
25 | Set_Global;
| ^~~~~~~~~~
either make "V" an input in the Global contract or initialize it before use
This is because the generated contract for Set_Global
is not precise
enough, and considers V
as an input of the procedure. Even if the body of
Set_Global
is not in SPARK, the user can easily provide the precise
information to GNATprove by adding a suitable contract to Set_Global
,
which requires to define an abstract state State
like in the previous
section:
procedure Set_Global with
Global => (Output => State),
Depends => (State => null);
With such a user contract on Set_Global
, GNATprove can verify the
contract of Set_Global_Conditionally
without false alarms.
7.4.1.4. Writing Dependency Contracts
Since GNATprove generates data and flow dependencies, you don’t need in general to add such contracts if you don’t want to.
The main reason to add such contracts is when you want GNATprove to verify that the implementation respects specified data dependencies and flow dependencies. For those projects submitted to certification, verification of data coupling and input/output relations may be a required verification objective, which can be achieved automatically with GNATprove provided the specifications are written as contracts.
Even if you write dependency contracts for the publicly visible subprograms, which describe the services offered by the unit, there is no need to write similar contracts on internal subprograms defined in the unit body. GNATprove can generate data and flow dependencies on these.
Also, as seen in the previous section, the data and flow dependencies generated by GNATprove may be imprecise, in which case it is necessary to add manual contracts to avoid false alarms.
7.4.2. Infeasible Subprogram Contracts
A contract is said to be infeasible if, for some values of its inputs
satisfying the precondition of the subprogram, there exists no values of its
outputs satisfying its postcondition. As an example of an infeasible (implict)
contract, consider the function Add
below. It states that it returns a valid
integer value equal to X + Y
for all valid integer values X
and Y
.
This is not possible for some valid values of X
and Y
, so this contract
is infeasible:
function Add (X, Y : Integer) return Integer is (X + Y);
Infeasible contracts are an issue when they occur on functions. Indeed, such functions can lead to the generation of an incorrect assumption which might invalidate the verification of every subprogram which directly or indirectly calls the function.
Generally, SPARK checks that subprograms correctly implement their implicit and explicit contracts, so infeasible contracts can only occur on subprograms which might not return normally on some inputs. As functions shall always terminate normally in SPARK, infeasible contracts on functions can never occur on a verified program entirely written in the SPARK subset. When working on code partially in another language, GNATprove also assumes that this is the case for subprograms that are not verified by the tool, see Managing Assumptions. Therefore, special care should be taken when Writing Contracts on Imported Subprograms.
To limit the impact of infeasible contracts, GNATprove inserts by default
implicit guards, so that potentially incorrect postconditions are only used on
input values on which the unverified subprogram is actually called. This is
not a full proof system however, so users should not rely on it to avoid
incorrect assumptions in the tool. What is more, these guards have a
non-negligible impact on prover performance. So if in your project, all
subprograms are in the SPARK subset, or you have confidence in the contracts
you wrote for the subprograms which are not in SPARK, you can disable these
guards using the --function-sandboxing=off
option.
Note
The effects of an infeasible contract can sometimes be detected by enabling
warnings produced by proof using the switch --proof-warnings=on
.
An incorrect assumption might cause branches and code snippets to be wrongly
flagged as dead by this mechanism.
7.4.3. Writing Contracts for Program Integrity
The most common use of contracts is to ensure program integrity, that is, the program keeps running within safe boundaries. For example, this includes the fact that the control flow of the program cannot be circumvented (e.g. through a buffer overflow vulnerability) and that data is not corrupted (e.g. data invariants are preserved).
Preconditions can be written to ensure program integrity, and in particular they ensure:
absence of run-time errors (AoRTE): no violations of language rules which would lead to raising an exception at run time (preconditions added to all subprograms which may raise a run-time error); and
defensive programming: no execution of a subprogram from an unexpected state (preconditions added to subprograms in the public API, to guard against possible misuse by client units); and
support of maintenance: prevent decrease in integrity (regressions, code rot) introduced during program evolution (preconditions added to internal subprograms, to guard against violations of the conditions to call these subprograms inside the unit itself); and
invariant checking: ensure key data invariants are maintained throughout execution (preconditions added to all subprograms which may break the invariant).
For example, unit Integrity
contains examples of all four kinds of
preconditions:
Precondition
X >= 0
on procedureSeen_One
ensures AoRTE, as otherwise a negative value forX
would cause the call toUpdate
to fail a range check, asUpdate
expects a non-negative value for its parameter.Precondition
X < Y
on procedureSeen_Two
ensures defensive programming, as the logic of the procedure is only correctly updating global variablesMax1
andMax2
to the two maximal values seen if parametersX
andY
are given in strictly increasing order.Precondition
X > Max2
on procedureUpdate
ensures support of maintenance, as this internal procedure relies on this condition on its parameter to operate properly.Precondition
Invariant
on procedureUpdate
ensures invariant checking, as the property thatMax2
is less thanMax1
expressed inInvariant
should be always respected.
1pragma Assertion_Policy (Pre => Check);
2
3package Integrity with
4 SPARK_Mode
5is
6 procedure Seen_One (X : Integer) with
7 Pre => X >= 0; -- AoRTE
8
9 procedure Seen_Two (X, Y : Natural) with
10 Pre => X < Y; -- defensive programming
11
12end Integrity;
1package body Integrity with
2 SPARK_Mode
3is
4 Max1 : Natural := 0; -- max value seen
5 Max2 : Natural := 0; -- second max value seen
6
7 function Invariant return Boolean is
8 (Max2 <= Max1);
9
10 procedure Update (X : Natural) with
11 Pre => X > Max2 and then -- support of maintenance
12 Invariant -- invariant checking
13 is
14 begin
15 if X > Max1 then
16 Max2 := Max1;
17 Max1 := X;
18 elsif X < Max1 then
19 Max2 := X;
20 end if;
21 end Update;
22
23 procedure Seen_One (X : Integer) is
24 begin
25 if X > Max2 then
26 Update (X);
27 end if;
28 end Seen_One;
29
30 procedure Seen_Two (X, Y : Natural) is
31 begin
32 if X > Max1 then
33 Max1 := Y;
34 Max2 := X;
35 elsif X > Max2 then
36 Update (Y);
37 Seen_One (X);
38 else
39 Seen_One (Y);
40 end if;
41 end Seen_Two;
42
43end Integrity;
Note that pragma Assertion_Policy (Pre => Check)
in integrity.ads
ensures that the preconditions on the public procedures Seen_One
and
Seen_Two
are always enabled at run time, while the precondition on internal
subprogram Update
is only enabled at run time if compiled with switch
-gnata
(typically set only for debugging or testing). GNATprove always
takes contracts into account, whatever value of Assertion_Policy
.
GNATprove cannot verify that all preconditions on Integrity
are
respected. Namely, it cannot verify that the call to Update
inside
Seen_One
respects its precondition, as it is not known from the calling
context that Invariant
holds:
integrity.adb:26:10: high: precondition might fail, cannot prove Invariant
26 | Update (X);
| ^~~~~~~~~
e.g. when Max1 = 0
and Max2 = 1
possible fix: precondition of subprogram at integrity.ads:6 should mention Max1 and Max2
6 | procedure Seen_One (X : Integer) with
| ^ here
Note that, although Invariant
is not required to hold either on entry to
Seen_Two
, the tests performed in if-statements in the body of Seen_Two
ensure that Invariant
holds when calling Update
inside Seen_Two
.
To prove completely the integrity of unit Integrity
, it is sufficient to
add Invariant
as a precondition and postcondition on every subprogram which
modifies the value of global variables Max1
and Max2
:
1pragma Assertion_Policy (Pre => Check);
2
3package Integrity_Proved with
4 SPARK_Mode
5is
6 procedure Seen_One (X : Integer) with
7 Pre => X >= 0 and then -- AoRTE
8 Invariant, -- invariant checking
9 Post => Invariant; -- invariant checking
10
11 procedure Seen_Two (X, Y : Natural) with
12 Pre => X < Y and then -- defensive programming
13 Invariant, -- invariant checking
14 Post => Invariant; -- invariant checking
15
16 function Invariant return Boolean;
17
18end Integrity_Proved;
1package body Integrity_Proved with
2 SPARK_Mode
3is
4 Max1 : Natural := 0; -- max value seen
5 Max2 : Natural := 0; -- second max value seen
6
7 function Invariant return Boolean is (Max2 <= Max1);
8
9 procedure Update (X : Natural) with
10 Pre => X > Max2 and then -- support of maintenance
11 Invariant, -- invariant checking
12 Post => Invariant -- invariant checking
13 is
14 begin
15 if X > Max1 then
16 Max2 := Max1;
17 Max1 := X;
18 elsif X < Max1 then
19 Max2 := X;
20 end if;
21 end Update;
22
23 procedure Seen_One (X : Integer) is
24 begin
25 if X > Max2 then
26 Update (X);
27 end if;
28 end Seen_One;
29
30 procedure Seen_Two (X, Y : Natural) is
31 begin
32 if X > Max1 then
33 Max1 := Y;
34 Max2 := X;
35 elsif X > Max2 then
36 Update (Y);
37 Seen_One (X);
38 else
39 Seen_One (Y);
40 end if;
41 end Seen_Two;
42
43end Integrity_Proved;
Here is the result of running GNATprove:
integrity_proved.adb:12:14: info: postcondition proved
integrity_proved.adb:26:10: info: precondition proved
integrity_proved.adb:26:18: info: range check proved
integrity_proved.adb:36:10: info: precondition proved
integrity_proved.adb:37:10: info: precondition proved
integrity_proved.adb:39:10: info: precondition proved
integrity_proved.ads:9:14: info: postcondition proved
integrity_proved.ads:14:14: info: postcondition proved
integrity_proved.ads:16:13: info: implicit aspect Always_Terminates on "Invariant" has been proved, subprogram will terminate
7.4.4. Writing Contracts for Functional Correctness
Going beyond program integrity, it is possible to express functional properties of the program as subprogram contracts. Such a contract can express either partially or completely the behavior of the subprogram. Typical simple functional properties express the range/constraints for parameters on entry and exit of subprograms (encoding their type-state), and the state of the module/program on entry and exit of subprograms (encoding a safety or security automaton). For those projects submitted to certification, expressing a subprogram requirement or specification as a complete functional contract allows GNATprove to verify automatically the implementation against the requirement/specification.
For example, unit Functional
is the same as Integrity_Proved
seen
previously, with additional functional contracts:
The postcondition on procedure
Update
(expressed as aPost
aspect) is a complete functional description of the behavior of the subprogram. Note the use of an if-expression.The postcondition on procedure
Seen_Two
(expressed as aPost
aspect) is a partial functional description of the behavior of the subprogram.The postcondition on procedure
Seen_One
(expressed as aContract_Cases
aspect) is a complete functional description of the behavior of the subprogram. There are three cases which correspond to different possible behaviors depending on the values of parameterX
and global variablesMax1
andMax2
. The benefit of expressing the postcondition as contract cases is both the gain in readability (no need to use'Old
for the guards, as in the postcondition ofUpdate
) and the automatic verification that the cases are disjoint and complete.
Note that global variables Max1
and Max2
are referred to through public
accessor functions Max_Value_Seen
and Second_Max_Value_Seen
. These
accessor functions can be declared after the contracts in which they appear, as
contracts are semantically analyzed only at the end of package declaration.
1pragma Assertion_Policy (Pre => Check);
2
3package Functional with
4 SPARK_Mode
5is
6 procedure Seen_One (X : Integer) with
7 Pre => X >= 0 and then -- AoRTE
8 Invariant, -- invariant checking
9 Post => Invariant, -- invariant checking
10 Contract_Cases => -- full functional
11 (X > Max_Value_Seen =>
12 -- max value updated
13 Max_Value_Seen = X and
14 Second_Max_Value_Seen = Max_Value_Seen'Old,
15 X > Second_Max_Value_Seen and
16 X < Max_Value_Seen =>
17 -- second max value updated
18 Max_Value_Seen = Max_Value_Seen'Old and
19 Second_Max_Value_Seen = X,
20 X = Max_Value_Seen or
21 X <= Second_Max_Value_Seen =>
22 -- no value updated
23 Max_Value_Seen = Max_Value_Seen'Old and
24 Second_Max_Value_Seen = Second_Max_Value_Seen'Old);
25
26 procedure Seen_Two (X, Y : Natural) with
27 Pre => X < Y and then -- defensive programming
28 Invariant, -- invariant checking
29 Post => Invariant and then -- invariant checking
30 Max_Value_Seen > 0 and then -- partial functional
31 Max_Value_Seen /= Second_Max_Value_Seen;
32
33 function Invariant return Boolean;
34
35 function Max_Value_Seen return Integer;
36
37 function Second_Max_Value_Seen return Integer;
38
39end Functional;
1package body Functional with
2 SPARK_Mode
3is
4 Max1 : Natural := 0; -- max value seen
5 Max2 : Natural := 0; -- second max value seen
6
7 function Invariant return Boolean is (Max2 <= Max1);
8
9 function Max_Value_Seen return Integer is (Max1);
10
11 function Second_Max_Value_Seen return Integer is (Max2);
12
13 procedure Update (X : Natural) with
14 Pre => X > Max2 and then -- support of maintenance
15 Invariant, -- invariant checking
16 Post => Invariant and then -- invariant checking
17 (if X > Max1'Old then -- complete functional
18 Max2 = Max1'Old and Max1 = X
19 elsif X < Max1'Old then
20 Max2 = X and Max1 = Max1'Old
21 else
22 Max2 = Max2'Old and Max1 = Max1'Old)
23 is
24 begin
25 if X > Max1 then
26 Max2 := Max1;
27 Max1 := X;
28 elsif X < Max1 then
29 Max2 := X;
30 end if;
31 end Update;
32
33 procedure Seen_One (X : Integer) is
34 begin
35 if X > Max2 then
36 Update (X);
37 end if;
38 end Seen_One;
39
40 procedure Seen_Two (X, Y : Natural) is
41 begin
42 if X > Max1 then
43 Max1 := Y;
44 Max2 := X;
45 elsif X > Max2 then
46 Update (Y);
47 Seen_One (X);
48 else
49 Seen_One (Y);
50 end if;
51 end Seen_Two;
52
53end Functional;
GNATprove manages to prove automatically almost all of these functional
contracts, except for the postcondition of Seen_Two
(note in particular the
proof that the contract cases for Seen_One
on line 10 are disjoint and
complete):
functional.ads:31:14: medium: postcondition might fail, cannot prove Max_Value_Seen /= Second_Max_Value_Seen
31 | Max_Value_Seen /= Second_Max_Value_Seen;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
e.g. when Max1 = 2
and Max2 = 2
The counterexample displayed for the postcondition not proved corresponds to a
case where Max1 = Max2 = 2
on entry to procedure Seen_Two
. By
highlighting the path for the counterexample in GNAT Studio (see Running GNATprove from GNAT Studio), the values of parameters for this counterexample are also
displayed, here X = 0
and Y = 1
. With these values, Max1
and Max2
would still be equal to 2 on exit, thus violating the part of the postcondition
stating that Max_Value_Seen /= Second_Max_Value_Seen
.
Another way to see it is to run GNATprove in mode per_path
(see
Running GNATprove from the Command Line or Running GNATprove from GNAT Studio), and highlight the path on which the postcondition is not proved, which
shows that when the last branch of the if-statement is taken, the following
property is not proved:
functional.ads:31:14: medium: postcondition might fail, cannot prove Max_Value_Seen /= (Second_Max_Value_Seen)
The missing piece of information here is that Max1
and Max2
are never
equal, except when they are both zero (the initial value). This can be added to
function Invariant
as follows:
function Invariant return Boolean is
(if Max1 = 0 then Max2 = 0 else Max2 < Max1);
With this more precise definition for Invariant
, all contracts are now
proved by GNATprove:
functional_proved.adb:17:14: info: postcondition proved
functional_proved.adb:37:10: info: precondition proved
functional_proved.adb:37:18: info: range check proved
functional_proved.adb:47:10: info: precondition proved
functional_proved.adb:48:10: info: precondition proved
functional_proved.adb:50:10: info: precondition proved
functional_proved.ads:9:14: info: postcondition proved
functional_proved.ads:10:06: info: disjoint contract cases proved
functional_proved.ads:10:06: info: complete contract cases proved
functional_proved.ads:11:28: info: contract case proved
functional_proved.ads:16:28: info: contract case proved
functional_proved.ads:21:36: info: contract case proved
functional_proved.ads:29:14: info: postcondition proved
functional_proved.ads:33:13: info: implicit aspect Always_Terminates on "Invariant" has been proved, subprogram will terminate
functional_proved.ads:35:13: info: implicit aspect Always_Terminates on "Max_Value_Seen" has been proved, subprogram will terminate
functional_proved.ads:37:13: info: implicit aspect Always_Terminates on "Second_Max_Value_Seen" has been proved, subprogram will terminate
In general, it may be needed to further refine the preconditions of subprograms to be able to prove their functional postconditions, to express either specific constraints on their calling context, or invariants maintained throughout the execution.
7.4.5. Writing Contracts on Main Subprograms
Parameterless procedures and parameterless functions with Integer return type,
that are in their own compilation unit, are identified by GNATprove as
potential main subprograms. These subprograms are special because they can
serve as an entry point to the program. If a main subprogram has a
precondition, SPARK will generate a check that this precondition holds at the
beginning of the execution of the main subprogram, assuming the
Initial_Condition
aspects of all with’ed packages.
Note that apart from this additional check, main subprograms behave like any other subprogram. They can be called from anywhere, and their preconditions need to be checked when they are called.
7.4.6. Writing Contracts on Imported Subprograms
Contracts are particularly useful to specify the behavior of imported
subprograms, which cannot be analyzed by GNATprove. It is compulsory to
specify in data dependencies the global variables these imported subprograms
may read and/or write, otherwise GNATprove assumes null
data dependencies
(no global variable read or written). It is also compulsory to specify procedures
which may not terminate with aspect Always_Terminates
(see
Contracts for Termination), otherwise GNATprove assumes that imported
subprograms always terminate. Note that a function is in general expected to
terminate in SPARK, so functions that do otherwise should be replaced by
procedures with a suitable annotation.
Note
A subprogram whose implementation is not available to GNATprove, either because the corresponding unit body has not been developed yet, or because the unit body is not part of the files analyzed by GNATprove (see Specifying Files To Analyze and Excluding Files From Analysis), is treated by GNATprove like an imported subprogram. The latter includes in particular subprograms from library projects that are externally built.
Note
Intrinsic subprograms such as arithmetic operations and shift/rotate functions are handled specially by GNATprove. Except for shift/rotate operations with a user-provided functional contract (precondition, postcondition or contract cases) which are treated like regular functions.
For example, unit Gen_Imported_Global
is a modified version of the
Gen_Abstract_Global
unit seen previously in Generation of Dependency Contracts, where procedure Set_Global
is imported from C:
1package Gen_Imported_Global with
2 SPARK_Mode,
3 Abstract_State => (State with External =>
4 (Async_Writers,
5 Async_Readers => False,
6 Effective_Reads => False,
7 Effective_Writes => False))
8is
9 procedure Set_Global with
10 Import,
11 Convention => C,
12 Global => (Output => State),
13 Always_Terminates;
14
15 procedure Set_Global_Twice;
16
17 procedure Set_Global_Conditionally (X : Boolean) with
18 Global => (Output => State),
19 Depends => (State => X);
20
21end Gen_Imported_Global;
Note that we added data dependencies to procedure Set_Global
, which can
be used to analyze its callers. We did not add flow dependencies, as
they are the same as the auto completed ones (see Auto Completion for Incomplete Contracts).
1with System.Storage_Elements;
2
3package body Gen_Imported_Global with
4 SPARK_Mode,
5 Refined_State => (State => V)
6is
7 pragma Warnings (GNATprove, Off, "assuming correct volatile properties");
8 pragma Warnings (GNATprove, Off, "assuming no concurrent accesses");
9 V : Integer with
10 Size => 32,
11 Volatile,
12 Async_Writers => True,
13 Async_Readers => False,
14 Effective_Reads => False,
15 Effective_Writes => False,
16 Address => System.Storage_Elements.To_Address (16#8000_0000#);
17 pragma Warnings (GNATprove, On, "assuming correct volatile properties");
18 pragma Warnings (GNATprove, On, "assuming no concurrent accesses");
19
20 procedure Set_Global_Twice is
21 begin
22 Set_Global;
23 Set_Global;
24 end Set_Global_Twice;
25
26 procedure Set_Global_Conditionally (X : Boolean) with
27 Refined_Global => (Output => V),
28 Refined_Depends => (V => X)
29 is
30 begin
31 if X then
32 Set_Global;
33 else
34 V := 42;
35 end if;
36 end Set_Global_Conditionally;
37
38end Gen_Imported_Global;
Note that we added an Address
aspect to global variable V
, so that it
can be read/written from a C file; this also requires the variable to be
volatile, which in turn requires the abstract state to be marked as external.
GNATprove gives the same results on this unit as before: it issues warnings
for the possible error in Set_Global_Twice
and it verifies the contract
given by the user for Set_Global_Conditionally
:
gen_imported_global.adb:22:07: warning: statement has no effect
22 | Set_Global;
| ^~~~~~~~~~
gen_imported_global.adb:22:07: warning: "V" constituent of "State" is set by "Set_Global" but not used after the call
22 | Set_Global;
| ^~~~~~~~~~
It is also possible to add functional contracts on imported subprograms, which
GNATprove uses to prove properties of their callers. It is compulsory to
specify in a precondition the conditions for calling these imported subprograms
without errors, otherwise GNATprove assumes a default precondition of
True
(no constraints on the calling context). One benefit of these
contracts is that they are verified at run time when the corresponding
assertion is enabled in Ada (either with pragma Assertion_Policy
or
compilation switch -gnata
).
Note
A subprogram whose implementation is not in SPARK is treated by
GNATprove almost like an imported subprogram, except that coarse data and
flow dependencies are generated (see Coarse Generation for non-SPARK Subprograms). In particular, unless the user adds a precondition to such a
subprogram, GNATprove assumes a default precondition of True
.
For example, unit Functional_Imported
is a modified version of the
Functional_Proved
unit seen previously in Writing Contracts for Functional Correctness, where procedures Update
and Seen_One
are
imported from C:
1pragma Assertion_Policy (Pre => Check);
2
3package Functional_Imported with
4 SPARK_Mode,
5 Abstract_State => Max_And_Snd,
6 Initializes => Max_And_Snd
7is
8 procedure Seen_One (X : Integer) with
9 Import,
10 Convention => C,
11 Global => (In_Out => Max_And_Snd),
12 Always_Terminates,
13 Pre => X >= 0 and then -- AoRTE
14 Invariant, -- invariant checking
15 Post => Invariant, -- invariant checking
16 Contract_Cases => -- full functional
17 (X > Max_Value_Seen =>
18 -- max value updated
19 Max_Value_Seen = X and
20 Second_Max_Value_Seen = Max_Value_Seen'Old,
21 X > Second_Max_Value_Seen and
22 X < Max_Value_Seen =>
23 -- second max value updated
24 Max_Value_Seen = Max_Value_Seen'Old and
25 Second_Max_Value_Seen = X,
26 X = Max_Value_Seen or
27 X <= Second_Max_Value_Seen =>
28 -- no value updated
29 Max_Value_Seen = Max_Value_Seen'Old and
30 Second_Max_Value_Seen = Second_Max_Value_Seen'Old);
31
32 procedure Seen_Two (X, Y : Natural) with
33 Pre => X < Y and then -- defensive programming
34 Invariant, -- invariant checking
35 Post => Invariant and then -- invariant checking
36 Max_Value_Seen > 0 and then -- partial functional
37 Max_Value_Seen /= Second_Max_Value_Seen;
38
39 function Invariant return Boolean;
40
41 function Max_Value_Seen return Integer;
42
43 function Second_Max_Value_Seen return Integer;
44
45end Functional_Imported;
1with System.Storage_Elements;
2
3package body Functional_Imported with
4 SPARK_Mode,
5 Refined_State => (Max_And_Snd => (Max, Snd))
6is
7 Max : Natural := 0 -- max value seen
8 with Address => System.Storage_Elements.To_Address (16#8000_0000#),
9 Warnings => Off;
10
11 Snd : Natural := 0 -- second max value seen
12 with Address => System.Storage_Elements.To_Address (16#8000_0004#),
13 Warnings => Off;
14
15 function Invariant return Boolean is
16 (if Max = 0 then Snd = 0 else Snd < Max);
17
18 function Max_Value_Seen return Integer is (Max);
19
20 function Second_Max_Value_Seen return Integer is (Snd);
21
22 procedure Update (X : Natural) with
23 Import,
24 Convention => C,
25 Global => (In_Out => (Max, Snd)),
26 Always_Terminates,
27 Pre => X > Snd and then -- support of maintenance
28 Invariant, -- invariant checking
29 Post => Invariant and then -- invariant checking
30 (if X > Max'Old then -- complete functional
31 Snd = Max'Old and Max = X
32 elsif X < Max'Old then
33 Snd = X and Max = Max'Old
34 else
35 Snd = Snd'Old and Max = Max'Old);
36
37 procedure Seen_Two (X, Y : Natural) is
38 begin
39 if X > Max then
40 Max := Y;
41 Snd := X;
42 elsif X > Snd then
43 Update (Y);
44 Seen_One (X);
45 else
46 Seen_One (Y);
47 end if;
48 end Seen_Two;
49
50end Functional_Imported;
Note that we added data dependencies to the imported procedures, as
GNATprove would assume otherwise incorrectly null
data dependencies.
As before, all contracts are proved by GNATprove:
functional_imported.adb:43:10: info: precondition proved
functional_imported.adb:44:10: info: precondition proved
functional_imported.adb:46:10: info: precondition proved
functional_imported.ads:6:03: info: flow dependencies proved
functional_imported.ads:16:06: info: disjoint contract cases proved
functional_imported.ads:16:06: info: complete contract cases proved
functional_imported.ads:35:14: info: postcondition proved
functional_imported.ads:39:13: info: implicit aspect Always_Terminates on "Invariant" has been proved, subprogram will terminate
functional_imported.ads:41:13: info: implicit aspect Always_Terminates on "Max_Value_Seen" has been proved, subprogram will terminate
functional_imported.ads:43:13: info: implicit aspect Always_Terminates on "Second_Max_Value_Seen" has been proved, subprogram will terminate
7.4.7. Contextual Analysis of Subprograms Without Contracts
It may be convenient to create local subprograms without necessarily specifying a contract for these. GNATprove attempts to perform a contextual analysis of these local subprograms without contract, at each call site, as if the code of the subprograms was inlined. Thus, the analysis proceeds in that case as if it had the most precise contract for the local subprogram, in the context of its calls.
Let’s consider as previously a subprogram which adds two to its integer input:
1package Arith_With_Local_Subp
2 with SPARK_Mode
3is
4 procedure Add_Two (X : in out Integer) with
5 Pre => X <= Integer'Last - 2,
6 Post => X = X'Old + 2;
7
8end Arith_With_Local_Subp;
And let’s implement it by calling two local subprograms without contracts (which may or not have a separate declaration), which each increment the input by one:
1package body Arith_With_Local_Subp
2 with SPARK_Mode
3is
4 -- Local procedure without external visibility
5 procedure Increment_In_Body (X : in out Integer) is
6 begin
7 X := X + 1;
8 end Increment_In_Body;
9
10 procedure Add_Two (X : in out Integer) is
11
12 -- Local procedure defined inside Add_Two
13 procedure Increment_Nested (X : in out Integer) is
14 begin
15 X := X + 1;
16 end Increment_Nested;
17
18 begin
19 Increment_In_Body (X);
20 Increment_Nested (X);
21 end Add_Two;
22
23end Arith_With_Local_Subp;
GNATprove would not be able to prove that the addition in
Increment_In_Body
or Increment_Nested
cannot overflow in any
context. If it was using only the default contract for these subprograms, it
also would not prove that the contract of Add_Two
is respected. But since
it analyzes these subprograms in the context of their calls only, it proves
here that no overflow is possible, and that the two increments correctly
implement the contract of Add_Two
:
1arith_with_local_subp.adb:7:14: info: overflow check proved, in call inlined at arith_with_local_subp.adb:19
2arith_with_local_subp.adb:15:17: info: overflow check proved, in call inlined at arith_with_local_subp.adb:20
3arith_with_local_subp.ads:6:14: info: postcondition proved
4arith_with_local_subp.ads:6:24: info: overflow check proved
This contextual analysis is available only for regular functions (not expression functions) or procedures that are not externally visible (not declared in the public part of the unit), without contracts (any of Global, Depends, Pre, Post, Contract_Cases), and respect the following conditions:
not dispatching
not marked
No_Return
not a generic instance
not defined in a generic instance
not defined in a protected type
without a parameter of unconstrained record type with discriminant dependent components
without a parameter or result of deep type (access type or composite type containing an access type)
not a traversal function
without an annotation to skip part of the analysis (see Annotation for Skipping Parts of the Analysis for an Entity)
without an annotation to hide or unhide information on another entity (see Pruning the Proof Context on a Case by Case Basis)
Subprograms that respects all of the above conditions are candidates for contextual analysis, and calls to such subprograms are inlined provided the subprogram and its calls respect the following additional conditions:
does not contain nested subprogram or package declarations or instantiations
not recursive
not called in an assertion or a contract
not called in a potentially unevaluated context
not called before its body is seen
If any of the above conditions is violated, GNATprove issues an info message to explain why the subprogram could not be analyzed in the context of its calls, and then proceeds to analyze it normally, using the default contract. Otherwise, both flow analysis and proof are done for the subprogram in the context of its calls.
Note that it is very simple to prevent contextual analysis of a local
subprogram, by adding a contract to it, for example a simple Pre => True
or
Global => null
. To prevent contextual analysis of all subprograms, pass the
switch --no-inlining
to GNATprove. This may be convenient during
development if the ultimate goal is to add contracts to subprograms to analyze
them separately, as contextual analysis may cause the analysis to take much
more time and memory.
7.4.8. Subprogram Termination
GNATprove can be used to verify the termination of subprograms. It will do it
unconditionnally for regular functions and package elaboration (which shall
have no side effects in SPARK), and on demand for procedures, entries and
functions with side effects (see Aspect Side_Effects). In the following
example, we specify that the five procedures should terminate using the
Always_Terminates
aspect (see Contracts for Termination):
1package Terminating_Annotations with SPARK_Mode is
2
3 procedure P_Rec (X : Natural) with
4 Always_Terminates;
5
6 procedure P_While (X : Natural) with
7 Always_Terminates;
8
9 procedure P_Not_SPARK (X : Natural) with
10 Always_Terminates;
11
12 procedure Not_SPARK (X : Natural);
13 procedure P_Call (X : Natural) with
14 Always_Terminates;
15
16 procedure P_Term (X : Natural) with
17 Always_Terminates,
18 Subprogram_Variant => (Decreases => X);
19end Terminating_Annotations;
To verify these annotations, GNATprove will look for while loops with no loop variants, recursive calls, and calls to procedures or entries which are not known to terminate. If it cannot make sure that the annotated subprogram will always terminate, it will then emit a failed check. As an example, let us consider the following implementation of the five procedures:
1package body Terminating_Annotations with SPARK_Mode is
2
3 procedure P_Rec (X : Natural) is
4 begin
5 if X = 0 then
6 return;
7 else
8 P_Rec (X - 1);
9 end if;
10 end P_Rec;
11
12 procedure P_While (X : Natural) is
13 Y : Natural := X;
14 begin
15 while Y > 0 loop
16 Y := Y - 1;
17 end loop;
18 end P_While;
19
20 procedure P_Not_SPARK (X : Natural) with SPARK_Mode => Off is
21 Y : Natural := X;
22 begin
23 while Y > 0 loop
24 Y := Y - 1;
25 end loop;
26 end P_Not_SPARK;
27
28 procedure Not_SPARK (X : Natural) with SPARK_Mode => Off is
29 begin
30 null;
31 end Not_SPARK;
32
33 procedure P_Call (X : Natural) is
34 begin
35 Not_SPARK (X);
36 end P_Call;
37
38 procedure P_Term (X : Natural) is
39 Y : Natural := X;
40 begin
41 P_Rec (Y);
42 P_While (Y);
43 P_Not_SPARK (Y);
44 P_Call (Y);
45
46 while Y > 0 loop
47 pragma Loop_Variant (Decreases => Y);
48 Y := Y - 1;
49 end loop;
50
51 if X = 0 then
52 return;
53 else
54 P_Term (X - 1);
55 end if;
56 end P_Term;
57end Terminating_Annotations;
As can be easily verified by review, all these procedures terminate.
However, GNATprove will fail to verify that P_Rec
,
P_While
, and P_Call
always terminate:
1
2terminating_annotations.adb:8:10: medium: aspect Always_Terminates on "P_Rec" could be incorrect, subprogram is recursive
3 8 | P_Rec (X - 1);
4 | ^~~~~~~~~~~~
5 possible fix: annotate "P_Rec" with a Subprogram_Variant aspect
6
7terminating_annotations.adb:15:19: medium: aspect Always_Terminates on "P_While" could be incorrect, loop might be nonterminating
8 15 | while Y > 0 loop
9 | ^~~~
10 possible fix: add loop variant in the loop body
11
12terminating_annotations.adb:35:07: medium: aspect Always_Terminates on "P_Call" could be incorrect, call to "Not_SPARK" might be nonterminating
13 35 | Not_SPARK (X);
14 | ^~~~~~~~~~~~
15 possible fix: annotate "Not_SPARK" with aspect Always_Terminates
Let us look at each procedure to understand what happens. The procedure
P_Rec
is recursive, and P_While
contains a while loop. Both cases
can theoretically lead to an infinite path in the subprogram, which is why
GNATprove cannot verify that they terminate. GNATprove does not complain
about not being able to verify the termination of P_Not_SPARK
. Clearly, it
is not because it could verify it, as it contains exactly the same loop as
P_While
. It is because, as the body of P_Not_SPARK
has been excluded
from analysis using SPARK_Mode => Off
, GNATprove does not attempt to
prove that it terminates. When looking at the body of P_Call
, we can see
that it calls a procedure Not_SPARK
. Clearly, this procedure always
returns, as it does not do anything. But, as the body of No_SPARK
has
been hidden from analysis using SPARK_Mode => Off
, GNATprove cannot
deduce that it terminates. As a result, it stays in the safe side, and assumes
that Not_SPARK
could loop, which causes the verification of P_Call
to
fail. Finally, GNATprove is able to verify that P_Term
terminates,
though it contains both a while loop and a recursive call. Indeed, we have
bounded both the number of possible iterations of the loop and the number of
recursive calls using a Loop_Variant
(for the loop iterations) and a
Subprogram_Variant
(for the recursive calls). Also note that, though it was
not able to prove termination of P_Rec
, P_While
, and P_Call
,
GNATprove will still trust the annotation when verifying P_Term
.