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.

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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package Only_Data_Dependencies with
  SPARK_Mode
is
   V : Integer;

   procedure Add (X : Integer) with
     Global => (In_Out => V);

   procedure Swap (X : in out Integer) with
     Global => (In_Out => V);

   procedure Call_Add (X, Y : Integer) with
     Global  => (In_Out => V),
     Depends => (V =>+ (X, Y));

   procedure Call_Swap (X, Y : in out Integer) with
     Global  => (In_Out => V),
     Depends => (X => Y, Y => X, V => V);

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
package body Only_Data_Dependencies with
  SPARK_Mode
is
   procedure Add (X : Integer) is
   begin
      V := V + X;
   end Add;

   procedure Swap (X : in out Integer) is
      Tmp : constant Integer := V;
   begin
      V := X;
      X := Tmp;
   end Swap;

   procedure Call_Add (X, Y : Integer) is
   begin
      Add (X);
      Add (Y);
   end Call_Add;

   procedure Call_Swap (X, Y : in out Integer) is
   begin
      Swap (X);
      Swap (Y);
      Swap (X);
   end Call_Swap;

end 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: medium: overflow check might fail
    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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package Only_Flow_Dependencies with
  SPARK_Mode
is
   V : Integer;

   procedure Add (X : Integer) with
     Depends => (V =>+ X);

   procedure Swap (X : in out Integer) with
     Depends => (V => X, X => V);

   procedure Call_Add (X, Y : Integer) with
     Global  => (In_Out => V),
     Depends => (V =>+ (X, Y));

   procedure Call_Swap (X, Y : in out Integer) with
     Global  => (In_Out => V),
     Depends => (X => Y, Y => X, V => V);

end Only_Flow_Dependencies;

The body of the unit is the same as before:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
package body Only_Flow_Dependencies with
  SPARK_Mode
is
   procedure Add (X : Integer) is
   begin
      V := V + X;
   end Add;

   procedure Swap (X : in out Integer) is
      Tmp : constant Integer := V;
   begin
      V := X;
      X := Tmp;
   end Swap;

   procedure Call_Add (X, Y : Integer) is
   begin
      Add (X);
      Add (Y);
   end Call_Add;

   procedure Call_Swap (X, Y : in out Integer) is
   begin
      Swap (X);
      Swap (Y);
      Swap (X);
   end Call_Swap;

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package Gen_Global with
  SPARK_Mode
is
   procedure Set_Global;

   procedure Do_Nothing;

   procedure Set_Global_Twice;

end Gen_Global;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
package body Gen_Global with
  SPARK_Mode
is
   V : Boolean;

   procedure Set_Global is
   begin
      V := True;
   end Set_Global;

   procedure Do_Nothing is
   begin
      null;
   end Do_Nothing;

   procedure Set_Global_Twice is
   begin
      Set_Global;
      Set_Global;
   end Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Global  => (Output => V),
     Depends => (V => X)
   is
   begin
      if X then
         Set_Global;
      else
         V := False;
      end if;
   end Set_Global_Conditionally;

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
package Gen_Abstract_Global with
  SPARK_Mode,
  Abstract_State => State
is
   procedure Set_Global;

   procedure Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Global  => (Output => State),
     Depends => (State => X);

end Gen_Abstract_Global;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
package body Gen_Abstract_Global with
  SPARK_Mode,
  Refined_State => (State => V)
is
   V : Boolean;

   procedure Set_Global is
   begin
      V := True;
   end Set_Global;

   procedure Set_Global_Twice is
   begin
      Set_Global;
      Set_Global;
   end Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Refined_Global  => (Output => V),
     Refined_Depends => (V => X)
   is
   begin
      if X then
         Set_Global;
      else
         V := False;
      end if;
   end Set_Global_Conditionally;

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
package Gen_Refined_Global with
  SPARK_Mode,
  Abstract_State => State
is
   procedure Set_Global with
     Global => (Output => State);

   procedure Set_Global_Twice with
     Global => (Output => State);

   procedure Set_Global_Conditionally (X : Boolean) with
     Global  => (Output => State),
     Depends => (State => X);

end Gen_Refined_Global;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
package body Gen_Refined_Global with
  SPARK_Mode,
  Refined_State => (State => V)
is
   V : Boolean;

   procedure Set_Global is
   begin
      V := True;
   end Set_Global;

   procedure Set_Global_Twice is
   begin
      Set_Global;
      Set_Global;
   end Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) is
   begin
      if X then
         Set_Global;
      else
         Set_Global;
      end if;
   end Set_Global_Conditionally;

end 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:

1
2
3
4
5
6
7
8
package Gen_Ada_Global with
  SPARK_Mode
is
   procedure Set_Global;

   procedure Set_Global_Twice;

end Gen_Ada_Global;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
package body Gen_Ada_Global with
  SPARK_Mode
is
   V : Boolean;

   procedure Set_Global with
     SPARK_Mode => Off
   is
   begin
      V := True;
   end Set_Global;

   procedure Set_Global_Twice is
   begin
      Set_Global;
      Set_Global;
   end Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Global  => (Output => V),
     Depends => (V => X)
   is
   begin
      if X then
         Set_Global;
      else
         V := False;
      end if;
   end Set_Global_Conditionally;

end 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 initialized
   25 |         Set_Global;
      |         ^~~~~~~~~~
  "V" is not an input in the Global contract of subprogram "Set_Global_Conditionally" at line 19
  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. 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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
pragma Assertion_Policy (Pre => Check);

package Integrity with
  SPARK_Mode
is
   procedure Seen_One (X : Integer) with
     Pre => X >= 0;  --  AoRTE

   procedure Seen_Two (X, Y : Natural) with
     Pre => X < Y;  --  defensive programming

end Integrity;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
package body Integrity with
  SPARK_Mode
is
   Max1 : Natural := 0;  --  max value seen
   Max2 : Natural := 0;  --  second max value seen

   function Invariant return Boolean is
      (Max2 <= Max1);

   procedure Update (X : Natural) with
     Pre => X > Max2 and then  --  support of maintenance
            Invariant          --  invariant checking
   is
   begin
      if X > Max1 then
         Max2 := Max1;
         Max1 := X;
      elsif X < Max1 then
         Max2 := X;
      end if;
   end Update;

   procedure Seen_One (X : Integer) is
   begin
      if X > Max2 then
         Update (X);
      end if;
   end Seen_One;

   procedure Seen_Two (X, Y : Natural) is
   begin
      if X > Max1 then
         Max1 := Y;
         Max2 := X;
      elsif X > Max2 then
         Update (Y);
         Seen_One (X);
      else
         Seen_One (Y);
      end if;
   end Seen_Two;

end 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: medium: precondition might fail, cannot prove (Invariant)
   26 |         Update (X);
      |         ^~~~~~~~~
  e.g. when Max1 = 0
        and Max2 = 1
        and X = 2
  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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
pragma Assertion_Policy (Pre => Check);

package Integrity_Proved with
  SPARK_Mode
is
   procedure Seen_One (X : Integer) with
     Pre  => X >= 0 and then   --  AoRTE
             Invariant,        --  invariant checking
     Post => Invariant;        --  invariant checking

   procedure Seen_Two (X, Y : Natural) with
     Pre  => X < Y and then    --  defensive programming
             Invariant,        --  invariant checking
     Post => Invariant;        --  invariant checking

   function Invariant return Boolean;

end Integrity_Proved;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
package body Integrity_Proved with
  SPARK_Mode
is
   Max1 : Natural := 0;  --  max value seen
   Max2 : Natural := 0;  --  second max value seen

   function Invariant return Boolean is (Max2 <= Max1);

   procedure Update (X : Natural) with
     Pre  => X > Max2 and then  --  support of maintenance
             Invariant,         --  invariant checking
     Post => Invariant          --  invariant checking
   is
   begin
      if X > Max1 then
         Max2 := Max1;
         Max1 := X;
      elsif X < Max1 then
         Max2 := X;
      end if;
   end Update;

   procedure Seen_One (X : Integer) is
   begin
      if X > Max2 then
         Update (X);
      end if;
   end Seen_One;

   procedure Seen_Two (X, Y : Natural) is
   begin
      if X > Max1 then
         Max1 := Y;
         Max2 := X;
      elsif X > Max2 then
         Update (Y);
         Seen_One (X);
      else
         Seen_One (Y);
      end if;
   end Seen_Two;

end 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

7.4.3. 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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
pragma Assertion_Policy (Pre => Check);

package Functional with
  SPARK_Mode
is
   procedure Seen_One (X : Integer) with
     Pre  => X >= 0 and then   --  AoRTE
             Invariant,        --  invariant checking
     Post => Invariant,        --  invariant checking
     Contract_Cases =>         --  full functional
       (X > Max_Value_Seen =>
          --  max value updated
          Max_Value_Seen = X and
          Second_Max_Value_Seen = Max_Value_Seen'Old,
        X > Second_Max_Value_Seen and
        X < Max_Value_Seen =>
          --  second max value updated
          Max_Value_Seen = Max_Value_Seen'Old and
          Second_Max_Value_Seen = X,
        X = Max_Value_Seen or
        X <= Second_Max_Value_Seen =>
          --  no value updated
          Max_Value_Seen = Max_Value_Seen'Old and
          Second_Max_Value_Seen = Second_Max_Value_Seen'Old);

   procedure Seen_Two (X, Y : Natural) with
     Pre  => X < Y and then               --  defensive programming
             Invariant,                   --  invariant checking
     Post => Invariant and then           --  invariant checking
             Max_Value_Seen > 0 and then  --  partial functional
             Max_Value_Seen /= Second_Max_Value_Seen;

   function Invariant return Boolean;

   function Max_Value_Seen return Integer;

   function Second_Max_Value_Seen return Integer;

end Functional;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
package body Functional with
  SPARK_Mode
is
   Max1 : Natural := 0;  --  max value seen
   Max2 : Natural := 0;  --  second max value seen

   function Invariant return Boolean is (Max2 <= Max1);

   function Max_Value_Seen return Integer is (Max1);

   function Second_Max_Value_Seen return Integer is (Max2);

   procedure Update (X : Natural) with
     Pre  => X > Max2 and then      --  support of maintenance
             Invariant,             --  invariant checking
     Post => Invariant and then     --  invariant checking
             (if X > Max1'Old then  --  complete functional
                Max2 = Max1'Old and Max1 = X
              elsif X < Max1'Old then
                Max2 = X and Max1 = Max1'Old
              else
                Max2 = Max2'Old and Max1 = Max1'Old)
   is
   begin
      if X > Max1 then
         Max2 := Max1;
         Max1 := X;
      elsif X < Max1 then
         Max2 := X;
      end if;
   end Update;

   procedure Seen_One (X : Integer) is
   begin
      if X > Max2 then
         Update (X);
      end if;
   end Seen_One;

   procedure Seen_Two (X, Y : Natural) is
   begin
      if X > Max1 then
         Max1 := Y;
         Max2 := X;
      elsif X > Max2 then
         Update (Y);
         Seen_One (X);
      else
         Seen_One (Y);
      end if;
   end Seen_Two;

end 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 = Natural'Last
        and Max2 = Natural'Last

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

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.4. 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.5. 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).

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.

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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package Gen_Imported_Global with
  SPARK_Mode,
  Abstract_State => (State with External =>
                        (Async_Writers,
                         Async_Readers => False,
                         Effective_Reads => False,
                         Effective_Writes => False))
is
   procedure Set_Global with
     Import,
     Convention => C,
     Global => (Output => State);

   procedure Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Global  => (Output => State),
     Depends => (State => X);

end 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).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
with System.Storage_Elements;

package body Gen_Imported_Global with
  SPARK_Mode,
  Refined_State => (State => V)
is
   V : Integer with
     Size => 32,
     Volatile,
     Async_Writers => True,
     Async_Readers => False,
     Effective_Reads => False,
     Effective_Writes => False,
     Address => System.Storage_Elements.To_Address (16#8000_0000#);

   procedure Set_Global_Twice is
   begin
      Set_Global;
      Set_Global;
   end Set_Global_Twice;

   procedure Set_Global_Conditionally (X : Boolean) with
     Refined_Global  => (Output => V),
     Refined_Depends => (V => X)
   is
   begin
      if X then
         Set_Global;
      else
         V := 42;
      end if;
   end Set_Global_Conditionally;

end 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:14:06: warning: writing to "V" is assumed to have no effects on other non-volatile objects
   14 |     Address => System.Storage_Elements.To_Address (16#8000_0000#);
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

gen_imported_global.adb:18:07: warning: statement has no effect
   18 |      Set_Global;
      |      ^~~~~~~~~~

gen_imported_global.adb:18:07: warning: "V" constituent of "State" is set by "Set_Global" but not used after the call
   18 |      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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
pragma Assertion_Policy (Pre => Check);

package Functional_Imported with
  SPARK_Mode,
  Abstract_State => Max_And_Snd,
  Initializes => Max_And_Snd
is
   procedure Seen_One (X : Integer) with
     Import,
     Convention => C,
     Global => (In_Out => Max_And_Snd),
     Pre  => X >= 0 and then   --  AoRTE
             Invariant,        --  invariant checking
     Post => Invariant,        --  invariant checking
     Contract_Cases =>         --  full functional
       (X > Max_Value_Seen =>
          --  max value updated
          Max_Value_Seen = X and
          Second_Max_Value_Seen = Max_Value_Seen'Old,
        X > Second_Max_Value_Seen and
        X < Max_Value_Seen =>
          --  second max value updated
          Max_Value_Seen = Max_Value_Seen'Old and
          Second_Max_Value_Seen = X,
        X = Max_Value_Seen or
        X <= Second_Max_Value_Seen =>
          --  no value updated
          Max_Value_Seen = Max_Value_Seen'Old and
          Second_Max_Value_Seen = Second_Max_Value_Seen'Old);

   procedure Seen_Two (X, Y : Natural) with
     Pre  => X < Y and then               --  defensive programming
             Invariant,                   --  invariant checking
     Post => Invariant and then           --  invariant checking
             Max_Value_Seen > 0 and then  --  partial functional
             Max_Value_Seen /= Second_Max_Value_Seen;

   function Invariant return Boolean;

   function Max_Value_Seen return Integer;

   function Second_Max_Value_Seen return Integer;

end Functional_Imported;

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
with System.Storage_Elements;

package body Functional_Imported with
  SPARK_Mode,
  Refined_State => (Max_And_Snd => (Max, Snd))
is
   pragma Warnings(Off, "indirect writes");
   pragma Warnings(Off, "writing to");
   Max : Natural := 0;  --  max value seen
   pragma Annotate(Gnatprove, Intentional, "constraints on bit representation", "");
   for Max'Address use System.Storage_Elements.To_Address (16#8000_0000#);

   Snd : Natural := 0;  --  second max value seen
   pragma Annotate(Gnatprove, Intentional, "constraints on bit representation", "");
   for Snd'Address use System.Storage_Elements.To_Address (16#8000_0004#);
   pragma Warnings(On, "indirect writes");
   pragma Warnings(On, "writing to");

   function Invariant return Boolean is
     (if Max = 0 then Snd = 0 else Snd < Max);

   function Max_Value_Seen return Integer is (Max);

   function Second_Max_Value_Seen return Integer is (Snd);

   procedure Update (X : Natural) with
     Import,
     Convention => C,
     Global => (In_Out => (Max, Snd)),
     Pre  => X > Snd and then      --  support of maintenance
             Invariant,            --  invariant checking
     Post => Invariant and then    --  invariant checking
             (if X > Max'Old then  --  complete functional
                Snd = Max'Old and Max = X
              elsif X < Max'Old then
                Snd = X and Max = Max'Old
              else
                Snd = Snd'Old and Max = Max'Old);

   procedure Seen_Two (X, Y : Natural) is
   begin
      if X > Max then
         Max := Y;
         Snd := X;
      elsif X > Snd then
         Update (Y);
         Seen_One (X);
      else
         Seen_One (Y);
      end if;
   end Seen_Two;

end Functional_Imported;

Note that we added data dependencies to the imported procedures, as GNATprove would assume otherwise incorrectly null data dependencies. The example also suppresses some GNATprove messages related to the address clause of the variable, which are not relevant to the example.

As before, all contracts are proved by GNATprove:

functional_imported.adb:46:10: info: precondition proved
functional_imported.adb:47:10: info: precondition proved
functional_imported.adb:49:10: info: precondition proved
functional_imported.ads:6:03: info: flow dependencies proved
functional_imported.ads:15:06: info: disjoint contract cases proved
functional_imported.ads:15:06: info: complete contract cases proved
functional_imported.ads:34:14: info: postcondition proved

7.4.6. 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:

1
2
3
4
5
6
7
8
package Arith_With_Local_Subp
  with SPARK_Mode
is
   procedure Add_Two (X : in out Integer) with
     Pre  => X <= Integer'Last - 2,
     Post => X = X'Old + 2;

end 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package body Arith_With_Local_Subp
  with SPARK_Mode
is
   --  Local procedure without external visibility
   procedure Increment_In_Body (X : in out Integer) is
   begin
      X := X + 1;
   end Increment_In_Body;

   procedure Add_Two (X : in out Integer) is

      --  Local procedure defined inside Add_Two
      procedure Increment_Nested (X : in out Integer) is
      begin
         X := X + 1;
      end Increment_Nested;

   begin
      Increment_In_Body (X);
      Increment_Nested (X);
   end Add_Two;

end 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:

1
2
3
4
arith_with_local_subp.adb:7:14: info: overflow check proved, in call inlined at arith_with_local_subp.adb:19
arith_with_local_subp.adb:15:17: info: overflow check proved, in call inlined at arith_with_local_subp.adb:20
arith_with_local_subp.ads:6:14: info: postcondition proved
arith_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

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

  • has a single point of return at the end of the subprogram

  • 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.7. Subprogram Termination

GNATprove is only concerned with partial correctness of subprograms, that is, it only checks that the contract of a subprogram holds when it terminates normally. What is more, GNATprove will enforce that no exception will be raised at runtime. Together, these two points ensure that every SPARK subprogram formally verified using GNATprove will always return normally in a state that respects its postcondition, as long as it terminates.

In general, GNATprove does not attempt to verify termination of subprograms. It can be instructed to do so using a GNATprove specific Annotate pragma. On the following example, we instruct GNATprove that the five F functions should terminate:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
package Terminating_Annotations with SPARK_Mode is

   function F_Rec (X : Natural) return Natural;
   pragma Annotate (GNATprove, Terminating, F_Rec);

   function F_While (X : Natural) return Natural;
   pragma Annotate (GNATprove, Terminating, F_While);

   function F_Not_SPARK (X : Natural) return Natural;
   pragma Annotate (GNATprove, Terminating, F_Not_SPARK);

   procedure Not_SPARK (X : Natural);
   function F_Call (X : Natural) return Natural;
   pragma Annotate (GNATprove, Terminating, F_Call);

   function F_Term (X : Natural) return Natural;
   pragma Annotate (GNATprove, Terminating, F_Term);
end Terminating_Annotations;

If every subprogram in a package is terminating, the package itself can be annotated with the terminating annotation. If the annotation is located on a generic package, then it should be valid for every instance of the package.

An aspect can be used instead of a pragma for both packages and subprograms:

package Pack with
   Annotate => (GNATprove, Terminating)
is
   procedure Proc with
     Annotate => (GNATprove, Terminating);
...

If a subprogram in SPARK is explicitly annotated as terminating, flow analysis will attempt to make sure that all the paths through the subprogram effectively return. In effect, it will look for while loops with no loop variants, recursive calls and calls to subprograms which are not known to be terminating. If GNATprove cannot make sure that the annotated subprogram is always terminating, it will then emit a failed check. As an example, let us consider the following implementation of the five F functions:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
package body Terminating_Annotations with SPARK_Mode is

   function F_Rec (X : Natural) return Natural is
   begin
      if X = 0 then
         return 0;
      else
         return F_Rec (X - 1);
      end if;
   end F_Rec;

   function F_While (X : Natural) return Natural is
      Y : Natural := X;
   begin
      while Y > 0 loop
         Y := Y - 1;
      end loop;
      return Y;
   end F_While;

   function F_Not_SPARK (X : Natural) return Natural with SPARK_Mode => Off is
      Y : Natural := X;
   begin
      while Y > 0 loop
         Y := Y - 1;
      end loop;
      return Y;
   end F_Not_SPARK;

   procedure Not_SPARK (X : Natural) with SPARK_Mode => Off is
   begin
      null;
   end Not_SPARK;

   function F_Call (X : Natural) return Natural is
   begin
      Not_SPARK (X);
      return 0;
   end F_Call;

   function F_Term (X : Natural) return Natural is
      Y : Natural := X;
   begin
      Y := F_Rec (Y);
      Y := F_While (Y);
      Y := F_Not_SPARK (Y);
      Y := F_Call (Y);

      while Y > 0 loop
         pragma Loop_Variant (Decreases => Y);
         Y := Y - 1;
      end loop;
      return Y;
   end F_Term;
end Terminating_Annotations;

As can be easily verified by review, all these functions terminate, and all return 0. As can be seen below, GNATprove will fail to verify that F_Rec, F_While, and F_Call terminate.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

terminating_annotations.adb:8:10: medium: "F_Rec" is recursive, terminating annotation could be incorrect
    8 |         return F_Rec (X - 1);
      |         ^~~~~~~~~~~~~~~~~~~

terminating_annotations.adb:15:19: medium: loop might be nonterminating, terminating annotation on "F_While" could be incorrect
   15 |      while Y > 0 loop
      |                  ^~~~

terminating_annotations.adb:37:07: medium: call to "Not_SPARK" might be nonterminating, terminating annotation on "F_Call" could be incorrect
   37 |      Not_SPARK (X);
      |      ^~~~~~~~~~~~

Let us look at each function to understand what happens. The function F_Rec is recursive, and the function F_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 F_Not_SPARK. Clearly, it is not because it could verify it, as it contains exactly the same loop as F_While. It is because, as the body of F_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 F_Call, we can see that it calls a procedure Not_SPARK. Clearly, this procedure is terminating, 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 F_Call to fail. Finally, GNATprove is able to verify that F_Term terminates, though it contains a while loop. Indeed, the number of possible iterations of the loop has been bounded using a Loop_Variant. Also note that, though it was not able to prove termination of F_Rec, F_While, and F_Call, GNATprove will still trust the annotation and consider them as terminating when verifying F_Term.

Note

Possible nontermination of a subprogram may influence GNATprove proof capabilities. Indeed, to avoid soundness issues due to nontermination in logical formulas, GNATprove will not be able to see the contract of nonterminating functions if they are called from definitions of constants, from contracts, or from assertions. In such a case, an information message will be emitted, stating that (implicit) contracts of the function are not available for proof. This message won’t appear if a Terminating annotation is supplied for the function as explained above.