5.2. Subprogram Contracts

The most important feature to specify the intended behavior of a SPARK program is the ability to attach a contract to subprograms. In this document, a subprogram can be a procedure, a function or a protected entry. This contract is made up of various optional parts:

  • The precondition introduced by aspect Pre specifies constraints on callers of the subprogram.

  • The postcondition introduced by aspect Post specifies (partly or completely) the functional behavior of the subprogram.

  • The contract cases introduced by aspect Contract_Cases is a way to partition the behavior of a subprogram. It can replace or complement a precondition and a postcondition.

  • The data dependencies introduced by aspect Global specify the global data read and written by the subprogram.

  • The flow dependencies introduced by aspect Depends specify how subprogram outputs depend on subprogram inputs.

  • The exceptional contract introduced by aspect Exceptional_Cases specifies the exceptions that might be propagated by a procedure, along with exceptional postconditions.

  • The termination contract introduced by aspect Always_Terminates requires procedures and entries to terminate, possibly under a particular condition.

  • The subprogram variant introduced by aspect Subprogram_Variant is used to ensure termination of recursive subprograms.

Which contracts to write for a given verification objective, and how GNATprove generates default contracts, is detailed in How to Write Subprogram Contracts.

GNATprove formally verifies that each execution of each SPARK subprogram it analyzes will either:

  • return normally in a state that respects the subprogram’s postcondition,

  • raise an exception in a state that respects the subprogram’s exceptional contract,

  • terminate abnormally as a result of a primary stack, secondary stack, or heap memory allocation failure, or

  • not terminate at all when it is allowed by its termination contract.

GNATprove also checks that procedures that are marked with aspect or pragma No_Return do not return: they should either raise an exception, call a non-returning subprogram, or loop forever on any input.

5.2.1. Preconditions

[Ada 2012]

The precondition of a subprogram specifies constraints on callers of the subprogram. Typically, preconditions are written as conjunctions of constraints that fall in one of the following categories:

  • exclusion of forbidden values of parameter, for example X /= 0 or Y not in Active_States

  • specification of allowed parameter values, for example X in 1 .. 10 or Y in Idle_States

  • relations that should hold between parameter values, for example (if Y in Active_State then Z /= Null_State)

  • expected values of global variables denoting the state of the computation, for example Current_State in Active_States

  • invariants about the global state that should hold when calling this subprogram, for example Is_Complete (State_Mapping)

  • relations involving the global state and input parameters that should hold when calling this subprogram, for example X in Next_States (Global_Map, Y)

When the program is compiled with assertions (for example with switch -gnata in GNAT), the precondition of a subprogram is checked at run time every time the subprogram is called. An exception is raised if the precondition fails. Not all assertions need to be enabled though. For example, a common idiom is to enable only preconditions (and not other assertions) in the production binary, by setting pragma Assertion_Policy as follows:

pragma Assertion_Policy (Pre => Check);

When a subprogram is analyzed with GNATprove, its precondition is used to restrict the contexts in which it may be executed, which is required in general to prove that the subprogram’s implementation:

In particular, the default precondition of True used by GNATprove when no explicit one is given may not be precise enough, unless it can be analyzed in the context of its callers by GNATprove (see Contextual Analysis of Subprograms Without Contracts). When a caller is analyzed with GNATprove, it checks that the precondition of the called subprogram holds at the point of call. And even when the implementation of the subprogram is not analyzed with GNATprove, it may be necessary to add a precondition to the subprogram for analyzing its callers (see Writing Contracts on Imported Subprograms).

For example, consider the procedure Add_To_Total which increments global counter Total by the value given in parameter Incr. To ensure that there are no integer overflows in the implementation, Incr should not be too large, which a user can express with the following precondition:

procedure Add_To_Total (Incr : in Integer) with
  Pre => Incr >= 0 and then Total <= Integer'Last - Incr;

To ensure that the value of Total remains non-negative, one should also add the condition Total >= 0 to the precondition:

procedure Add_To_Total (Incr : in Integer) with
  Pre => Incr >= 0 and then Total in 0 .. Integer'Last - Incr;

Finally, GNATprove also analyzes preconditions to ensure that they are free from run-time errors in all contexts. This may require writing the precondition in a special way. For example, the precondition of Add_To_Total above uses the shortcut boolean operator and then instead of and, so that calling the procedure in a context where Incr is negative does not result in an overflow when evaluating Integer'Last - Incr. Instead, the use of and then ensures that a precondition failure will occur before the expression Integer'Last - Incr is evaluated.

Note

It is good practice to use the shortcut boolean operator and then instead of and in preconditions. This is required in some cases by GNATprove to prove absence of run-time errors inside preconditions.

Raise expressions occuring in preconditions are handled in a special way. Indeed, it is a common pattern to use a raise expression to change the exception raised by a failed precondition. To support this use case, raising an expression in a precondition is considered in SPARK to be a failure of the precondition, as opposed to a runtime failure, which would not be allowed in SPARK. As an example, we may want to introduce specific exceptions for the the failure of each part of the precondition of Add_To_Total, so as to debug them more easily. This can be done by using two raise expressions as in the following snippet:

Negative_Increment  : exception;
Total_Out_Of_Bounds : exception;

procedure Add_To_Total (Incr : in Integer) with
  Pre => (Incr >= 0 or else raise Negative_Increment)
  and then (Total in 0 .. Integer'Last - Incr
            or else raise Total_Out_Of_Bounds);

The raise expressions are associated to each conjunct using an or else short circuit operator, so that they will be evaluated when the conjunct evaluates to False and the exception will be raised.

On this code, GNATprove will not attempt to verify that the exceptions can never be raised when evaluating the precondition in any context, like it does for other runtime exceptions. Instead, it will consider them being raised as a failure of the precondition. So, for GNATprove, the precondition with the raise expressions above is effectively equivalent to the precondition of the previous example.

5.2.2. Postconditions

[Ada 2012]

The postcondition of a subprogram specifies partly or completely the functional behavior of the subprogram. Typically, postconditions are written as conjunctions of properties that fall in one of the following categories:

  • possible values returned by a function, using the special attribute Result (see Attribute Result), for example Get'Result in Active_States

  • possible values of output parameters, for example Y in Active_States

  • expected relations between output parameter values, for example if Success then Y /= Null_State

  • expected relations between input and output parameter values, possibly using the special attribute Old (see Attribute Old), for example if Success then Y /= Y'Old

  • expected values of global variables denoting updates to the state of the computation, for example Current_State in Active_States

  • invariants about the global state that should hold when returning from this subprogram, for example Is_Complete (State_Mapping)

  • relations involving the global state and output parameters that should hold when returning from this subprogram, for example X in Next_States (Global_Map, Y)

When the program is compiled with assertions (for example with switch -gnata in GNAT), the postcondition of a subprogram is checked at run time every time the subprogram returns. An exception is raised if the postcondition fails. Usually, postconditions are enabled during tests, as they provide dynamically checkable oracles of the intended behavior of the program, and disabled in the production binary for efficiency.

When a subprogram is analyzed with GNATprove, it checks that the postcondition of a subprogram cannot fail. This verification is modular: GNATprove considers all calling contexts in which the precondition of the subprogram holds for the analysis of a subprogram. GNATprove also analyzes postconditions to ensure that they are free from run-time errors, like any other assertion.

For example, consider the procedure Add_To_Total which increments global counter Total with the value given in parameter Incr. This intended behavior can be expressed in its postcondition:

procedure Add_To_Total (Incr : in Integer) with
  Post => Total = Total'Old + Incr;

The postcondition of a subprogram is used to analyze calls to the subprograms. In particular, the default postcondition of True used by GNATprove when no explicit one is given may not be precise enough to prove properties of its callers, unless it analyzes the subprogam’s implementation in the context of its callers (see Contextual Analysis of Subprograms Without Contracts).

Recursive subprograms and mutually recursive subprograms are treated in this respect exactly like non-recursive ones. Provided the execution of these subprograms always terminates (a property that is not verified by GNATprove), then GNATprove correctly checks that their postcondition is respected by using this postcondition for recursive calls.

Special care should be exercized for functions that return a boolean, as a common mistake is to write the expected boolean result as the postcondition:

function Total_Above_Threshold (Threshold : in Integer) return Boolean with
  Post => Total > Threshold;

while the correct postcondition uses Attribute Result:

function Total_Above_Threshold (Threshold : in Integer) return Boolean with
  Post => Total_Above_Threshold'Result = Total > Threshold;

Both GNAT compiler and GNATprove issue a warning on the semantically correct but likely functionally wrong postcondition.

5.2.3. Contract Cases

[SPARK]

When a subprogram has a fixed set of different functional behaviors, it may be more convenient to specify these behaviors as contract cases rather than a postcondition. For example, consider a variant of procedure Add_To_Total which either increments global counter Total by the given parameter value when possible, or saturates at a given threshold. Each of these behaviors can be defined in a contract case as follows:

procedure Add_To_Total (Incr : in Integer) with
  Contract_Cases => (Total + Incr < Threshold  => Total = Total'Old + Incr,
                     Total + Incr >= Threshold => Total = Threshold);

Each contract case consists in a guard and a consequence separated by the symbol =>. When the guard evaluates to True on subprogram entry, the corresponding consequence should also evaluate to True on subprogram exit. We say that this contract case was enabled for the call. Exactly one contract case should be enabled for each call, or said equivalently, the contract cases should be disjoint and complete.

For example, the contract cases of Add_To_Total express that the subprogram should be called in two distinct cases only:

  • on inputs that can be added to Total to obtain a value strictly less than a given threshold, in which case Add_To_Total adds the input to Total.

  • on inputs whose addition to Total exceeds the given threshold, in which case Add_To_Total sets Total to the threshold value.

When the program is compiled with assertions (for example with switch -gnata in GNAT), all guards are evaluated on entry to the subprogram, and there is a run-time check that exactly one of them is True. For this enabled contract case, there is another run-time check when returning from the subprogram that the corresponding consequence evaluates to True.

When a subprogram is analyzed with GNATprove, it checks that there is always exactly one contract case enabled, and that the consequence of the contract case enabled cannot fail. If the subprogram also has a precondition, GNATprove performs these checks only for inputs that satisfy the precondition, otherwise for all inputs.

In the simple example presented above, there are various ways to express an equivalent postcondition, in particular using Conditional Expressions:

procedure Add_To_Total (Incr : in Integer) with
  Post => (if Total'Old + Incr < Threshold  then
             Total = Total'Old + Incr
           else
             Total = Threshold);

procedure Add_To_Total (Incr : in Integer) with
  Post => Total = (if Total'Old + Incr < Threshold then Total'Old + Incr else Threshold);

procedure Add_To_Total (Incr : in Integer) with
  Post => Total = Integer'Min (Total'Old + Incr, Threshold);

In general, an equivalent postcondition may be cumbersome to write and less readable. Contract cases also provide a way to automatically verify that the input space is partitioned in the specified cases, which may not be obvious with a single expression in a postcondition when there are many cases.

The guard of the last case may be others, to denote all cases not captured by previous contract cases. For example, the contract of Add_To_Total may be written:

procedure Add_To_Total (Incr : in Integer) with
  Contract_Cases => (Total + Incr < Threshold => Total = Total'Old + Incr,
                     others                   => Total = Threshold);

When others is used as a guard, there is no need for verification (both at run-time and using GNATprove) that the set of contract cases covers all possible inputs. Only disjointness of contract cases is checked in that case.

5.2.4. Data Dependencies

[SPARK]

The data dependencies of a subprogram specify the global data that a subprogram is allowed to read and write. Together with the parameters, they completely specify the inputs and outputs of a subprogram. Like parameters, the global variables mentioned in data dependencies have a mode: Input for inputs, Output for outputs and In_Out for global variables that are both inputs and outputs. A last mode of Proof_In is defined for inputs that are only read in contracts and assertions. For example, data dependencies can be specified for procedure Add_To_Total which increments global counter Total as follows:

procedure Add_To_Total (Incr : in Integer) with
  Global => (In_Out => Total);

For protected subprograms, the protected object is considered as an implicit parameter of the subprogram:

  • it is an implicit parameter of mode in of a protected function; and

  • it is an implicit parameter of mode in out of a protected procedure or a protected entry.

Data dependencies have no impact on compilation and the run-time behavior of a program. When a subprogram is analyzed with GNATprove, it checks that the implementation of the subprogram:

  • only reads global inputs mentioned in its data dependencies,

  • only writes global outputs mentioned in its data dependencies, and

  • always completely initializes global outputs that are not also inputs.

See Data Initialization Policy for more details on this analysis of GNATprove. During its analysis, GNATprove uses the specified data dependencies of callees to analyze callers, if present, otherwise a default data dependency contract is generated (see Generation of Dependency Contracts) for callees.

There are various benefits when specifying data dependencies on a subprogram, which gives various reasons for users to add such contracts:

  • GNATprove verifies automatically that the subprogram implementation respects the specified accesses to global data.

  • GNATprove uses the specified contract during flow analysis, to analyze the data and flow dependencies of the subprogram’s callers, which may result in a more precise analysis (less false alarms) than with the generated data dependencies.

  • GNATprove uses the specified contract during proof, to check absence of run-time errors and the functional contract of the subprogram’s callers, which may also result in a more precise analysis (less false alarms) than with the generated data dependencies.

When data dependencies are specified on a subprogram, they should mention all global data read and written in the subprogram. When a subprogram has neither global inputs nor global outputs, it can be specified using the null data dependencies:

function Get (X : T) return Integer with
  Global => null;

When a subprogram has only global inputs but no global outputs, it can be specified either using the Input mode:

function Get_Sum return Integer with
  Global => (Input => (X, Y, Z));

or equivalently without any mode:

function Get_Sum return Integer with
  Global => (X, Y, Z);

Note the use of parentheses around a list of global inputs or outputs for a given mode.

Global data that is both read and written should be mentioned with the In_Out mode, and not as both input and output. For example, the following data dependencies on Add_To_Total are illegal and rejected by GNATprove:

procedure Add_To_Total (Incr : in Integer) with
  Global => (Input  => Total,
             Output => Total);  --  INCORRECT

Global data that is partially written in the subprogram should also be mentioned with the In_Out mode, and not as an output. See Data Initialization Policy.

5.2.5. Flow Dependencies

[SPARK]

The flow dependencies of a subprogram specify how its outputs (both output parameters and global outputs) depend on its inputs (both input parameters and global inputs). For example, flow dependencies can be specified for procedure Add_To_Total which increments global counter Total as follows:

procedure Add_To_Total (Incr : in Integer) with
  Depends => (Total => (Total, Incr));

The above flow dependencies can be read as “the output value of global variable Total depends on the input values of global variable Total and parameter Incr”.

Outputs (both parameters and global variables) may have an implicit input part depending on their type:

  • an unconstrained array A has implicit input bounds A'First and A'Last

  • a discriminated record R has implicit input discriminants, for example R.Discr

Thus, an output array A and an output discriminated record R may appear in input position inside a flow-dependency contract, to denote the input value of the bounds (for the array) or the discriminants (for the record).

For protected subprograms, the protected object is considered as an implicit parameter of the subprogram which may be mentioned in the flow dependencies, under the name of the protected unit (type or object) being declared:

  • as an implicit parameter of mode in of a protected function, it can be mentioned on the right-hand side of flow dependencies; and

  • as an implicit parameter of mode in out of a protected procedure or a protected entry, it can be mentioned on both sides of flow dependencies.

Flow dependencies have no impact on compilation and the run-time behavior of a program. When a subprogram is analyzed with GNATprove, it checks that, in the implementation of the subprogram, outputs depend on inputs as specified in the flow dependencies. During its analysis, GNATprove uses the specified flow dependencies of callees to analyze callers, if present, otherwise a default flow dependency contract is generated for callees (see Generation of Dependency Contracts).

When flow dependencies are specified on a subprogram, they should mention all flows from inputs to outputs. In particular, the output value of a parameter or global variable that is partially written by a subprogram depends on its input value (see Data Initialization Policy).

When the output value of a parameter or global variable depends on its input value, the corresponding flow dependency can use the shorthand symbol + to denote that a variable’s output value depends on the variable’s input value plus any other input listed. For example, the flow dependencies of Add_To_Total above can be specified equivalently:

procedure Add_To_Total (Incr : in Integer) with
  Depends => (Total =>+ Incr);

When an output value depends on no input value, meaning that it is completely (re)initialized with constants that do not depend on variables, the corresponding flow dependency should use the null input list:

procedure Init_Total with
  Depends => (Total => null);

5.2.6. State Abstraction and Contracts

[SPARK]

The subprogram contracts mentioned so far always used directly global variables. In many cases, this is not possible because the global variables are defined in another unit and not directly visible (because they are defined in the private part of a package specification, or in a package implementation). The notion of abstract state in SPARK can be used in that case (see State Abstraction) to name in contracts global data that is not visible.

5.2.6.1. State Abstraction and Dependencies

Suppose the global variable Total incremented by procedure Add_To_Total is defined in the package implementation, and a procedure Cash_Tickets in a client package calls Add_To_Total. Package Account which defines Total can define an abstract state State that represents Total, as seen in State Abstraction, which allows using it in Cash_Tickets’s data and flow dependencies:

procedure Cash_Tickets (Tickets : Ticket_Array) with
  Global  => (Output => Account.State),
  Depends => (Account.State => Tickets);

As global variable Total is not visible from clients of unit Account, it is not visible either in the visible part of Account’s specification. Hence, externally visible subprograms in Account must also use abstract state State in their data and flow dependencies, for example:

procedure Init_Total with
  Global  => (Output => State),
  Depends => (State => null);

procedure Add_To_Total (Incr : in Integer) with
  Global  => (In_Out => State),
  Depends => (State =>+ Incr);

Then, the implementations of Init_Total and Add_To_Total can define refined data and flow dependencies introduced respectively by Refined_Global and Refined_Depends, which give the precise dependencies for these subprograms in terms of concrete variables:

procedure Init_Total with
  Refined_Global  => (Output => Total),
  Refined_Depends => (Total => null)
is
begin
   Total := 0;
end Init_Total;

procedure Add_To_Total (Incr : in Integer) with
  Refined_Global  => (In_Out => Total),
  Refined_Depends => (Total =>+ Incr)
is
begin
   Total := Total + Incr;
end Add_To_Total;

Here, the refined dependencies are the same as the abstract ones where State has been replaced by Total, but that’s not always the case, in particular when the abstract state is refined into multiple concrete variables (see State Abstraction). GNATprove checks that:

  • each abstract global input has at least one of its constituents mentioned by the concrete global inputs

  • each abstract global in_out has at least one of its constituents mentioned with mode input and one with mode output (or at least one constituent with mode in_out)

  • each abstract global output has to have all its constituents mentioned by the concrete global outputs

  • the concrete flow dependencies are a subset of the abstract flow dependencies

GNATprove uses the abstract contract (data and flow dependencies) of Init_Total and Add_To_Total when analyzing calls outside package Account and the more precise refined contract (refined data and flow dependencies) of Init_Total and Add_To_Total when analyzing calls inside package Account.

Refined dependencies can be specified on both subprograms and tasks for which data and/or flow dependencies that are specified include abstract states which are refined in the current unit.

5.2.6.2. State Abstraction and Functional Contracts

If global variables are not visible for data dependencies, they are not visible either for functional contracts. For example, in the case of procedure Add_To_Total, if global variable Total is not visible, we cannot express anymore the precondition and postcondition of Add_To_Total as in Preconditions and Postconditions. Instead, we define accessor functions to retrieve properties of the state that we need to express, and we use these in contracts. For example here:

function Get_Total return Integer;

procedure Add_To_Total (Incr : in Integer) with
  Pre  => Incr >= 0 and then Get_Total in 0 .. Integer'Last - Incr,
  Post => Get_Total = Get_Total'Old + Incr;

Function Get_Total may be defined either in the private part of package Account or in its implementation. It may take the form of a regular function or an expression function (see Expression Functions), for example:

Total : Integer;

function Get_Total return Integer is (Total);

Although no refined preconditions and postconditions are required on the implementation of Add_To_Total, it is possible to provide a refined postcondition introduced by Refined_Post in that case, which specifies a more precise functional behavior of the subprogram. For example, procedure Add_To_Total may also increment the value of a counter Call_Count at each call, which can be expressed in the refined postcondition:

procedure Add_To_Total (Incr : in Integer) with
  Refined_Post => Total = Total'Old + Incr and Call_Count = Call_Count'Old + 1
is
   ...
end Add_To_Total;

A refined postcondition can be given on a subprogram implementation even when the unit does not use state abstraction, and even when the default postcondition of True is used implicitly on the subprogram declaration.

GNATprove uses the abstract contract (precondition and postcondition) of Add_To_Total when analyzing calls outside package Account and the more precise refined contract (precondition and refined postcondition) of Add_To_Total when analyzing calls inside package Account.

5.2.7. Exceptional Contracts

[SPARK]

In SPARK, every procedure which might propagate an exception should be annotated with an exceptional contract. This contract, introduced by the Exceptional_Cases aspect, lists all the exceptions which might be propagated by a procedure, and associates them to an exceptional postcondition. This postcondition describes the effect of the procedure when the exception is raised. As an example, consider the procedure Incr_All below. It goes over an array to increment its elements. If an overflow would occur, the exception Overflow is raised and the traversal is stopped. The global variable Index is used to store the current index at this point. The exceptional contract of Incr_All states both that it might propagate Overflow, and that it will only do so if it finds an offending index, using the global variable Index. The fact that Overflow is necessarily raised when such an index exists follows from the regular postcondition of Incr_All:

 1procedure Exceptions with SPARK_Mode is
 2
 3   type Nat_Array is array (Positive range <>) of Natural;
 4
 5   Overflow : exception;
 6   Index    : Positive;
 7
 8   procedure Incr_All (A : in out Nat_Array) with
 9     Post =>
10       (for all I in A'Range => A'Old (I) /= Natural'Last
11          and then A (I) = A'Old (I) + 1),
12     Exceptional_Cases =>
13       (Overflow => Index in A'Old'Range and then A'Old (Index) = Natural'Last);
14
15   procedure Incr_All (A : in out Nat_Array) is
16   begin
17      for I in A'Range loop
18         if A (I) = Natural'Last then
19            Index := I;
20            raise Overflow;
21         end if;
22
23         A (I) := A (I) + 1;
24         pragma Loop_Invariant
25           (for all J in A'First .. I => A'Loop_Entry (J) < Natural'Last);
26         pragma Loop_Invariant
27           (for all J in A'First .. I => A (J) = A'Loop_Entry (J) + 1);
28      end loop;
29   end Incr_All;
30
31   procedure Incr_All_Cond (A : in out Nat_Array; Success : out Boolean) with
32     Post => Success = (for all I in A'Range => A'Old (I) /= Natural'Last)
33       and then
34         (if Success then (for all I in A'Range => A (I) = A'Old (I) + 1));
35
36   procedure Incr_All_Cond (A : in out Nat_Array; Success : out Boolean) is
37   begin
38      Incr_All (A);
39      Success := True;
40   exception
41      when Overflow =>
42	 A := (others => 0);
43         Success := False;
44   end Incr_All_Cond;
45
46   procedure Incr_All_With_Pre (A : in out Nat_Array) with
47     Pre  => (for all I in A'Range => A (I) /= Natural'Last),
48     Post =>
49       (for all I in A'Range => A'Old (I) /= Natural'Last
50          and then A (I) = A'Old (I) + 1);
51
52   procedure Incr_All_With_Pre (A : in out Nat_Array) is
53   begin
54      Incr_All (A);
55   end Incr_All_With_Pre;
56
57begin
58   null;
59end Exceptions;

GNATprove can successfully verify both Incr_All above and its two callers: the exception is handled inside Incr_All_Cond and the call to Incr_All never raises Overflow in Incr_All_With_Pre.

exceptions.adb:10:08: info: postcondition proved
exceptions.adb:10:40: info: index check proved
exceptions.adb:11:23: info: index check proved
exceptions.adb:11:35: info: index check proved
exceptions.adb:11:38: info: overflow check proved
exceptions.adb:13:21: info: exceptional case proved
exceptions.adb:13:58: info: index check proved
exceptions.adb:19:22: info: range check proved
exceptions.adb:23:25: info: overflow check proved
exceptions.adb:25:13: info: loop invariant initialization proved
exceptions.adb:25:13: info: loop invariant preservation proved
exceptions.adb:25:56: info: index check proved
exceptions.adb:27:13: info: loop invariant preservation proved
exceptions.adb:27:13: info: loop invariant initialization proved
exceptions.adb:27:45: info: index check proved
exceptions.adb:27:64: info: index check proved
exceptions.adb:27:67: info: overflow check proved
exceptions.adb:31:29: info: initialization of "A" proved
exceptions.adb:31:51: info: initialization of "Success" proved
exceptions.adb:32:14: info: postcondition proved
exceptions.adb:32:56: info: index check proved
exceptions.adb:34:55: info: index check proved
exceptions.adb:34:67: info: index check proved
exceptions.adb:34:70: info: overflow check proved
exceptions.adb:38:07: info: only expected exception raised
exceptions.adb:42:12: info: length check proved
exceptions.adb:47:42: info: index check proved
exceptions.adb:49:08: info: postcondition proved
exceptions.adb:49:40: info: index check proved
exceptions.adb:50:23: info: index check proved
exceptions.adb:50:35: info: index check proved
exceptions.adb:50:38: info: overflow check proved
exceptions.adb:54:07: info: only expected exception raised

The Data Initialization Policy of SPARK is mostly enforced on exceptional exit of subprograms. All global outputs shall be initialized when an exception is propagated, like Index in the example above. It is the case too for parameters which are necessarily passed by reference (tagged types, aliased parameters…). Other parameters, either necessarily passed by copy or for which the parameter passing mode is unspecified by the language, do not need to be initialized. As a result, after a call which has propagated an exception:

  • output parameters necessarily passed by reference are considered to have been initialized or updated by the call as on a normal return,

  • output parameters necessarily passed by copy are preserved, and

  • output parameters for which the parameter passing mode is unspecified by the language are considered to not be initialized anymore; they should not be read after the call.

As an example, the parameter A of Incr_All is a composite type containing only subcomponents of a by-copy type (a scalar). As per the Ada reference manual, its parameter passing mode is unspecified. It means that its value will be unspecified if the call to Incr_All raises an exception, as can be seen on Incr_All_Bad_Init:

 1procedure Exceptions_Bad_Init with SPARK_Mode is
 2
 3   type Nat_Array is array (Positive range <>) of Natural;
 4
 5   Overflow : exception;
 6   Index    : Positive;
 7
 8   procedure Incr_All (A : in out Nat_Array) with
 9     Import,
10     Global => (In_Out => Index),
11     Always_Terminates,
12     Post =>
13       (for all I in A'Range => A'Old (I) /= Natural'Last
14          and then A (I) = A'Old (I) + 1),
15     Exceptional_Cases =>
16       (Overflow => Index in A'Old'Range and then A'Old (Index) = Natural'Last);
17
18   procedure Incr_All_Bad_Init
19     (A       : in out Nat_Array;
20      Success : out Boolean;
21      N       : out Natural)
22   with
23     Post => Success = (for all I in A'Range => A'Old (I) /= Natural'Last)
24       and then
25         (if Success then (for all I in A'Range => A (I) = A'Old (I) + 1));
26
27   procedure Incr_All_Bad_Init
28     (A       : in out Nat_Array;
29      Success : out Boolean;
30      N       : out Natural)
31   is
32   begin
33      Incr_All (A);
34      Success := True;
35      N := 0;
36   exception
37      when Overflow =>
38         Success := False;
39         N := A (Index);
40   end Incr_All_Bad_Init;
41
42begin
43   null;
44end Exceptions_Bad_Init;


exceptions_bad_init.adb:19:07: medium: "A" might not be initialized in "Incr_All_Bad_Init"
   19 |     (A       : in out Nat_Array;
      |      ^ here
  reason for check: OUT parameter should be fully initialized on return
  possible fix: initialize "A" on all paths, make "A" an IN OUT parameter or annotate it with aspect Relaxed_Initialization

exceptions_bad_init.adb:23:49: medium: "A" might not be initialized
   23 |     Post => Success = (for all I in A'Range => A'Old (I) /= Natural'Last)
      |                                                ^ here

exceptions_bad_init.adb:39:15: high: "A" is not initialized
   39 |         N := A (Index);
      |              ^ here

Note that, even though access types are passed by copy, in parameters of an access-to-variable part can be safely used after an exceptional exit as only the designated value can be modified.

To make it easier for the user, it is not allowed to mention parameters which are not necessarily passed by reference in an exceptional postcondition. An error is emitted if the exceptional postcondition of Incr_All is modified to mention A:

 1procedure Exceptions_Bad with SPARK_Mode is
 2
 3   type Nat_Array is array (Positive range <>) of Natural;
 4
 5   Overflow : exception;
 6   Index    : Positive;
 7
 8   procedure Incr_All_Bad (A : in out Nat_Array) with
 9     Import,
10     Post =>
11       (for all I in A'Range => A'Old (I) /= Natural'Last
12          and then A (I) = A'Old (I) + 1),
13     Exceptional_Cases =>
14       (Overflow => A'Old (Index) = Natural'Last
15        and then (for all I in A'Range =>
16                        A (I) = (if I < Index then A'Old (I) + 1 else A'Old (I))));
17
18begin
19   null;
20end Exceptions_Bad;


exceptions_bad.adb:16:25: error: formal parameter of mode "in out" in consequence of Exceptional_Cases is not allowed in SPARK
   16 |                        A (I) = (if I < Index then A'Old (I) + 1 else A'Old (I))));
      |                        ^ here
  only parameters passed by reference are allowed
  violation of aspect SPARK_Mode at line 1
    1 |procedure Exceptions_Bad with SPARK_Mode is
      |                              ^ here
gnatprove: error during flow analysis and proof

The exceptional contract is allowed if the parameter A is marked as aliased however, as it is then necessarily passed by reference:

 1procedure Exceptions_Post with SPARK_Mode is
 2
 3   type Nat_Array is array (Positive range <>) of Natural;
 4
 5   Overflow : exception;
 6   Index    : Positive;
 7
 8   procedure Incr_All_Post (A : aliased in out Nat_Array) with
 9     Post =>
10       (for all I in A'Range => A'Old (I) /= Natural'Last
11          and then A (I) = A'Old (I) + 1),
12     Exceptional_Cases =>
13       (Overflow => A'Old (Index) = Natural'Last
14        and then (for all I in A'Range =>
15                        A (I) = (if I < Index then A'Old (I) + 1 else A'Old (I))));
16
17   procedure Incr_All_Post (A : aliased in out Nat_Array) is
18   begin
19      for I in A'Range loop
20         if A (I) = Natural'Last then
21            Index := I;
22            raise Overflow;
23         end if;
24
25         A (I) := A (I) + 1;
26         pragma Loop_Invariant
27           (for all J in A'First .. I => A'Loop_Entry (J) < Natural'Last);
28         pragma Loop_Invariant
29           (for all J in A'First .. I => A (J) = A'Loop_Entry (J) + 1);
30      end loop;
31   end Incr_All_Post;
32
33begin
34   null;
35end Exceptions_Post;

exceptions_post.adb:10:08: info: postcondition proved
exceptions_post.adb:10:40: info: index check proved
exceptions_post.adb:11:23: info: index check proved
exceptions_post.adb:11:35: info: index check proved
exceptions_post.adb:11:38: info: overflow check proved
exceptions_post.adb:13:21: info: exceptional case proved
exceptions_post.adb:13:28: info: index check proved
exceptions_post.adb:15:28: info: index check proved
exceptions_post.adb:15:59: info: index check proved
exceptions_post.adb:15:62: info: overflow check proved
exceptions_post.adb:15:78: info: index check proved
exceptions_post.adb:21:22: info: range check proved
exceptions_post.adb:25:25: info: overflow check proved
exceptions_post.adb:27:13: info: loop invariant initialization proved
exceptions_post.adb:27:13: info: loop invariant preservation proved
exceptions_post.adb:27:56: info: index check proved
exceptions_post.adb:29:13: info: loop invariant preservation proved
exceptions_post.adb:29:13: info: loop invariant initialization proved
exceptions_post.adb:29:45: info: index check proved
exceptions_post.adb:29:64: info: index check proved
exceptions_post.adb:29:67: info: overflow check proved

Note that only exceptions which are raised explicitly in the code can be handled or propagated. For example, it would not be possible to remove the defensive code raising the exception in the loop and instead propagate Constraint_Error directly as in Incr_All_CE. Indeed, GNATprove always attempts to prove that runtime checks never fail. It complains on Incr_All_CE that the range check might fail, and flags the exceptional case as unreachable if proof warnings are enabled:

 1procedure Exceptions_RTE with SPARK_Mode is
 2
 3   type Nat_Array is array (Positive range <>) of Natural;
 4
 5   procedure Incr_All_CE (A : in out Nat_Array) with
 6     Post =>
 7       (for all I in A'Range => A'Old (I) /= Natural'Last
 8          and then A (I) = A'Old (I) + 1),
 9     Exceptional_Cases => (Constraint_Error => True);
10
11   procedure Incr_All_CE (A : in out Nat_Array) is
12   begin
13      for I in A'Range loop
14         A (I) := A (I) + 1;
15         pragma Loop_Invariant
16           (for all J in A'First .. I => A'Loop_Entry (J) < Natural'Last);
17         pragma Loop_Invariant
18           (for all J in A'First .. I => A (J) = A'Loop_Entry (J) + 1);
19      end loop;
20   end Incr_All_CE;
21
22begin
23   null;
24end Exceptions_RTE;


exceptions_rte.adb:9:48: warning: unreachable branch
    9 |     Exceptional_Cases => (Constraint_Error => True);
      |                                               ^~~~

exceptions_rte.adb:14:25: high: overflow check might fail, cannot prove upper bound for A (I) + 1
   14 |         A (I) := A (I) + 1;
      |                  ~~~~~~^~~
  e.g. when A = (1 => Natural'Last)
        and A'First = 1
        and A'Last = 1
        and I = 1
  reason for check: result of addition must fit in a 32-bits machine integer

If the exception raised by a raise statement or procedure call is neither handled nor allowed by its exceptional contract (that is, it has no associated exceptional postcondition or this postcondition is statically False), then it is unexpected and GNATprove will make sure that it never occurs. More precisely, GNATprove treats raising an unexpected exception in the following way:

  • in flow analysis, the program paths that lead to a statement raising an unexpected exception are not considered when checking the contract of the subprogram; and

  • in proof, a check is generated for these statements, to prove that no such program point is reachable.

Occurences of pragma Assert (X) where X is an expression statically equivalent to False are treated in the same way.

As an example, consider the artificial subprogram Check_OK which raises an exception when parameter OK is False. The Check_OK procedure does not have an exceptional contract so the exception is unexpected:

 1package Abnormal_Terminations with
 2  SPARK_Mode
 3is
 4
 5   G1, G2 : Integer := 0;
 6
 7   procedure Check_OK (OK : Boolean) with
 8     Global => (Output => G1),
 9     Pre    => OK;
10
11end Abnormal_Terminations;

 1package body Abnormal_Terminations with
 2  SPARK_Mode
 3is
 4
 5   procedure Check_OK (OK : Boolean) is
 6   begin
 7      if OK then
 8         G1 := 1;
 9      else
10         G2 := 1;
11         raise Program_Error;
12      end if;
13   end Check_OK;
14
15end Abnormal_Terminations;

Note that, although G2 is assigned in Check_OK, its assignment is directly followed by a raise_statement, so G2 is never assigned on an execution of Check_OK that terminates normally. As a result, G2 is not mentioned in the data dependencies of Check_OK. During flow analysis, GNATprove verifies that the body of Check_OK implements its declared data dependencies.

During proof, GNATprove generates a check that the raise_statement on line 11 is never reached. Here, it is proved thanks to the precondition of Check_OK which states that parameter OK should always be True on entry:

abnormal_terminations.adb:11:10: info: only expected exception raised
abnormal_terminations.ads:8:06: info: data dependencies proved
abnormal_terminations.ads:8:27: info: initialization of "G1" proved

Note

Raising an exception is a side-effect. As a consequence, the aspect Exceptional_Cases is not allowed on functions and exceptions raised by raise_expressions cannot be handled or propagated. GNATprove makes sure that they never occur.

5.2.8. Contracts for Termination

[SPARK]

By default, GNATprove verifies termination of all functions and automatically instantiated lemmas (procedures annotated with Automatic_Instantiation). For procedures or entries, GNATprove does not attempt to verify termination and is only concerned with their partial correctness. This means that GNATprove only verifies that the contract of each procedure or entry holds whenever it terminates (i.e., returns or raises an exception). It is still possible that the subprogram does not terminate in some or all cases (it can for example loop forever or exit the whole program using GNAT.OS_Lib.OS_Exit).

The Always_Terminates GNAT specific aspect allows users to request that GNATprove also verifies that a procedure or entry terminates. It is the case for example of the procedures Ok_Terminating and Bad_Terminating below. The aspect can also be used to provide a boolean condition like for the Conditionally_Loop procedure. If this condition is present, then the proof of termination is only attempted when the condition evaluates to True on subprogram entry. As an example, the procedure Conditionally_Loop might not terminate if its Cond parameter evaluates to True, and Loop_Forever never needs to terminate (but it might):

 1package Possibly_Nonterminating with
 2  SPARK_Mode
 3is
 4
 5   procedure Loop_Forver with
 6     No_Return,
 7     Always_Terminates => False,
 8     Exceptional_Cases => (others => False);
 9
10   procedure Conditionally_Loop (Cond : Boolean) with
11     Always_Terminates => not Cond;
12
13   procedure OK_Terminating with
14     Always_Terminates;
15
16   procedure Bad_Terminating with
17     Always_Terminates;
18
19end Possibly_Nonterminating;

 1package body Possibly_Nonterminating with
 2  SPARK_Mode
 3is
 4   procedure Loop_Forver is
 5   begin
 6      loop
 7         null;
 8      end loop;
 9   end Loop_Forver;
10
11   procedure Conditionally_Loop (Cond : Boolean) is
12   begin
13      if Cond then
14         Loop_Forver;
15      end if;
16   end Conditionally_Loop;
17
18   procedure Ok_Terminating is
19   begin
20      Conditionally_Loop (False);
21   end Ok_Terminating;
22
23   procedure Bad_Terminating is
24   begin
25      Conditionally_Loop (True);
26   end Bad_Terminating;
27
28end Possibly_Nonterminating;

GNATprove verifies the termination of OK_Terminating and the conditional termination of Conditionally_Loop but a failed check is emitted for Bad_Terminating as it does not terminate.

possibly_nonterminating.adb:14:10: info: conditional call termination proved
possibly_nonterminating.adb:20:07: info: conditional call termination proved

possibly_nonterminating.adb:25:07: medium: call might not terminate
   25 |      Conditionally_Loop (True);
      |      ^~~~~~~~~~~~~~~~~~~~~~~~
  reason for check: procedure "Bad_Terminating" has an Always_Terminates aspect
possibly_nonterminating.ads:13:14: info: aspect Always_Terminates on "OK_Terminating" has been proved, subprogram will terminate
possibly_nonterminating.ads:16:14: info: aspect Always_Terminates on "Bad_Terminating" has been proved, subprogram will terminate

A package can also be annotated with the Always_Terminates aspect. It does not apply to the elaboration of the package, which should always terminate in SPARK, but serves as a default for all the procedures located inside: unless specified otherwise, a procedure declared inside a package annotated with Always_Terminates should always terminate.

5.2.9. Subprogram Variant

[SPARK]

To ensure termination of recursive subprograms, it is possible to annotate them using the aspect Subprogram_Variant. This aspect provides a value which should progress in some sense between the beginning of the subprogram and each recursive call. The value is associated to a direction, which can be either Increases or Decreases for numeric variants, or Structural for structural variants.

Numeric variants can take a discrete value or, in the case of the direction Decreases, a big natural (see Ada.Numerics.Big_Integers). On every recursive call, a check is generated to ensure that the value progresses (decreases or increases) with respect to its value at the beginning of the subprogram. Since a discrete value is necessarily bounded by its Ada type, and a big natural is always greater than 0, it is enough to ensure that there will be no infinite chain of recursive calls.

In the following example, we can verify that the Fibonacci function terminates stating that its parameter N decreases at each recursive call:

 1with SPARK.Big_Integers; use SPARK.Big_Integers;
 2
 3package Recursive_Subprograms with SPARK_Mode is
 4
 5   function Fibonacci (N : Big_Natural) return Big_Natural is
 6     (if N = 0 then 0
 7      elsif N = 1 then 1
 8      else Fibonacci (N - 1) + Fibonacci (N - 2))
 9   with Subprogram_Variant => (Decreases => N);
10end Recursive_Subprograms;

GNATprove generates one verification condition per recursive call to make sure that the value given for N is smaller than the value of N on entry of Fibonacci:

recursive_subprograms.ads:5:13: info: implicit aspect Always_Terminates on "Fibonacci" has been proved, subprogram will terminate
recursive_subprograms.ads:6:10: info: predicate check proved
recursive_subprograms.ads:6:14: info: predicate check proved
recursive_subprograms.ads:6:21: info: predicate check proved
recursive_subprograms.ads:7:13: info: predicate check proved
recursive_subprograms.ads:7:17: info: predicate check proved
recursive_subprograms.ads:7:24: info: predicate check proved
recursive_subprograms.ads:8:12: info: subprogram variant proved
recursive_subprograms.ads:8:12: info: predicate check proved
recursive_subprograms.ads:8:23: info: predicate check proved
recursive_subprograms.ads:8:25: info: predicate check proved
recursive_subprograms.ads:8:27: info: predicate check proved
recursive_subprograms.ads:8:30: info: predicate check proved
recursive_subprograms.ads:8:32: info: subprogram variant proved
recursive_subprograms.ads:8:32: info: predicate check proved
recursive_subprograms.ads:8:43: info: predicate check proved
recursive_subprograms.ads:8:45: info: predicate check proved
recursive_subprograms.ads:8:47: info: predicate check proved
recursive_subprograms.ads:9:45: info: range check proved

It is possible to give more than one numeric value in a subprogram variant. In this case, values are checked in the order in which they appear. If a value progresses (increases or decreases as specified) then it is enough to ensure the progression of the whole variant and the subsequent values are not considered. In the same way, if a value annotated with Increases actually decreases strictly (or the other way around) then the evaluation terminates and the verification of the variant fails. It is only if the values of all the preceding expressions have been found to be preserved that the subsequent value is considered. The function Max computes the index of the maximal value in a slice of an array. At each recursive call, it shifts the bound containing the smallest value:

 1package Recursive_Subprograms.Multiple with SPARK_Mode is
 2   type Nat_Array is array (Positive range <>) of Natural;
 3
 4   function Max (A : Nat_Array; F, L : Positive) return Positive is
 5     (if F = L then F
 6      elsif A (F) > A (L) then Max (A, F, L - 1)
 7      else Max (A, F + 1, L))
 8   with Pre  => L in A'Range and F in A'Range and F <= L,
 9        Post => Max'Result in F .. L
10         and then (for all I in F .. L => A (I) <= A (Max'Result)),
11        Subprogram_Variant => (Increases => F, Decreases => L);
12end Recursive_Subprograms.Multiple;

The variant specifies that, for each recursive call, either F increases, or F stays the same and L decreases. The order is not important here, as L and F are never modified at the same time. This variant can be verified by GNATprove.

recursive_subprograms-multiple.ads:4:13: info: implicit aspect Always_Terminates on "Max" has been proved, subprogram will terminate
recursive_subprograms-multiple.ads:6:16: info: index check proved
recursive_subprograms-multiple.ads:6:24: info: index check proved
recursive_subprograms-multiple.ads:6:32: info: precondition proved
recursive_subprograms-multiple.ads:6:32: info: subprogram variant proved
recursive_subprograms-multiple.ads:6:45: info: range check proved
recursive_subprograms-multiple.ads:7:12: info: precondition proved
recursive_subprograms-multiple.ads:7:12: info: subprogram variant proved
recursive_subprograms-multiple.ads:7:22: info: overflow check proved
recursive_subprograms-multiple.ads:9:17: info: postcondition proved
recursive_subprograms-multiple.ads:10:46: info: index check proved
recursive_subprograms-multiple.ads:10:58: info: index check proved

Structural variants are generally used on recursive data-structures. The value associated to such a variant is necessarily a formal parameter of the subprogram. On every recursive call, a check is generated to ensure that the actual parameter denoted by the variant designates a strict subcomponent of the formal parameter denoted the variant at the beggining of the call. Since, due to the Memory Ownership Policy of SPARK, the data-structures cannot contain cycles, it is enough to ensure that there will be no infinite chain of recursive calls.

In the following example, we can verify that the Length function on singly-linked lists terminates stating that the structure designated by its parameter L structurally decreases between two recursive calls:

 1with Ada.Numerics.Big_Numbers.Big_Integers;
 2use  Ada.Numerics.Big_Numbers.Big_Integers;
 3
 4package Recursive_Subprograms with SPARK_Mode is
 5   type Cell;
 6   type List is access Cell;
 7   type Cell is record
 8      Value : Integer;
 9      Next  : List;
10   end record;
11
12   function Length (L : List) return Big_Natural is
13     (if L = null then Big_Natural'(0) else Length (L.Next) + 1)
14   with Subprogram_Variant => (Structural => L);
15end Recursive_Subprograms;

The fact that the actual parameter for L on the recursive call designates a strict subcomponent of the structure designated by formal parameter L can be verified by GNATprove:

recursive_subprograms.ads:12:13: info: implicit aspect Always_Terminates on "Length" has been proved, subprogram will terminate
recursive_subprograms.ads:13:37: info: predicate check proved
recursive_subprograms.ads:13:45: info: subprogram variant proved
recursive_subprograms.ads:13:45: info: predicate check proved
recursive_subprograms.ads:13:54: info: pointer dereference check proved
recursive_subprograms.ads:13:61: info: predicate check proved
recursive_subprograms.ads:13:63: info: predicate check proved

Structural variants are subjects to a number of restrictions. They cannot be combined with other variants, and are checked according to a mostly syntactic criterion. When these restrictions cannot be followed, structural variants can be systematically replaced by a decreasing numeric variant providing the depth (or size) of the data structure, like function Length above. Strictly speaking, structural variants are only required to define the function returning that metric.

To verify the termination of mutually recursive subprograms, all subprograms should be annotated with compatible variants. We say that two variants are compatible if they have the same number of expressions, and matching values in the list have the same direction and the same base type. For example, the variants of Is_Even and Is_Odd are compatible, because both are of type Integer and both decrease.

 1package Recursive_Subprograms.Mutually with SPARK_Mode is
 2   function Is_Odd (X : Natural) return Boolean with
 3     Subprogram_Variant => (Decreases => X);
 4   function Is_Even (X : Natural) return Boolean with
 5     Subprogram_Variant => (Decreases => X);
 6
 7   function Is_Odd (X : Natural) return Boolean is
 8     (if X = 0 then False else not Is_Even (X - 1));
 9   function Is_Even (X : Natural) return Boolean is
10     (if X = 0 then True else not Is_Odd (X - 1));
11end Recursive_Subprograms.Mutually;

GNATprove introduces a check to make sure that the variant progresses at each mutually recursive call.

recursive_subprograms-mutually.ads:2:13: info: implicit aspect Always_Terminates on "Is_Odd" has been proved, subprogram will terminate
recursive_subprograms-mutually.ads:4:13: info: implicit aspect Always_Terminates on "Is_Even" has been proved, subprogram will terminate
recursive_subprograms-mutually.ads:8:36: info: subprogram variant proved
recursive_subprograms-mutually.ads:8:47: info: range check proved
recursive_subprograms-mutually.ads:10:35: info: subprogram variant proved
recursive_subprograms-mutually.ads:10:45: info: range check proved