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 of True (or False 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 procedure Seen_One ensures AoRTE, as otherwise a negative value for X would cause the call to Update to fail a range check, as Update expects a non-negative value for its parameter.

  • Precondition X < Y on procedure Seen_Two ensures defensive programming, as the logic of the procedure is only correctly updating global variables Max1 and Max2 to the two maximal values seen if parameters X and Y are given in strictly increasing order.

  • Precondition X > Max2 on procedure Update ensures support of maintenance, as this internal procedure relies on this condition on its parameter to operate properly.

  • Precondition Invariant on procedure Update ensures invariant checking, as the property that Max2 is less than Max1 expressed in Invariant 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 a Post 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 a Post aspect) is a partial functional description of the behavior of the subprogram.

  • The postcondition on procedure Seen_One (expressed as a Contract_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 parameter X and global variables Max1 and Max2. 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 of Update) 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.