5.3. Package Contracts

Subprograms are not the only entities to bear contracts in SPARK. Package contracts are made up of various optional parts:

  • The state abstraction specifies how global variables defined in the package are referred to abstractly where they are not visible. Aspect Abstract_State introduces abstract names and aspect Refined_State specifies the mapping between these names and global variables.

  • The package initialization introduced by aspect Initializes specifies which global data (global variables and abstract state) defined in the package is initialized at package startup.

  • The package initial condition introduced by aspect Initial_Condition specifies the properties holding after package startup.

Package startup (a.k.a. package elaboration in Ada RM) consists in the evaluation of all declarations in the package specification and implementation, in particular the evaluation of constant declarations and those variable declarations which contain an initialization expression, as well as the statements sometimes given at the end of a package body that are precisely executed at package startup.

5.3.1. State Abstraction

[SPARK]

The state abstraction of a package specifies a mapping between abstract names and concrete global variables defined in the package. State abstraction allows to define Subprogram Contracts at an abstract level that does not depend on a particular choice of implementation (see State Abstraction and Contracts), which is better both for maintenance (no need to change contracts) and scalability of analysis (contracts can be much smaller).

5.3.1.1. Basic State Abstraction

One abstract name may be mapped to more than one concrete variable, but no two abstract names can be mapped to the same concrete variable. When state abstraction is specified on a package, all non-visible global variables defined in the private part of the package specification and in its implementation should be mapped to abstract names. Thus, abstract names correspond to a partitioning of the non-visible global variables defined in the package.

The simplest use of state abstraction is to define a single abstract name (conventionally called State) to denote all non-visible global variables defined in the package. For example, consider package Account defining a global variable Total in its implementation, which is abstracted as State:

package Account with
  Abstract_State => State
is
   ...
end Account;

package body Account with
  Refined_State => (State => Total)
is
   Total : Integer;
   ...
end Account;

The aspect Refined_State maps each abstract name to a list of concrete global variables defined in the package. The list can be simply null to serve as placeholder for future definitions of global variables. Instead of concrete global variables, one can also use abstract names for the state of nested packages and private child packages, whose state is considered to be also defined in the parent package.

If global variable Total is defined in the private part of Account’s package specification, then the declaration of Total must use the special aspect Part_Of to declare its membership in abstract state State:

package Account with
  Abstract_State => State
is
   ...
private
  Total : Integer with Part_Of => State;
  ...
end Account;

This ensures that Account’s package specification can be checked by GNATprove even if its implementation is not in SPARK, or not available for analysis, or not yet developed.

A package with state abstraction must have a package body that states how abstract states are refined in aspect Refined_State, unless the package body is not in SPARK. If there is no other reason for the package to have a body, then one should use pragma Elaborate_Body in the package spec to make it legal for the package to have a body on which to express state refinement.

In general, an abstract name corresponds to multiple global variables defined in the package. For example, we can imagine adding global variables to log values passed in argument to procedure Add_To_Total, that are also mapped to abstract name State:

package Account with
  Abstract_State => State
is
   ...
end Account;

package body Account with
  Refined_State => (State => (Total, Log, Log_Size))
is
   Total    : Integer;
   Log      : Integer_Array;
   Log_Size : Natural;
   ...
end Account;

We can also imagine defining different abstract names for the total and the log:

package Account with
  Abstract_State => (State, Internal_State)
is
   ...
end Account;

package body Account with
  Refined_State => (State => Total,
                    Internal_State => (Log, Log_Size))
is
   Total    : Integer;
   Log      : Integer_Array;
   Log_Size : Natural;
   ...
end Account;

The abstract names defined in a package are visible everywhere the package name itself is visible:

  • in the scope where the package is declared, for a locally defined package

  • in units that have a clause with <package>;

  • in units that have a clause limited with <package>;

The last case allows subprograms in two packages to mutually reference the abstract state of the other package in their data and flow dependencies.

5.3.1.2. Special Cases of State Abstraction

Global constants with a statically known value are not part of a package’s state. On the contrary, constant with variable inputs are constants whose value depends on the value of either a variable or a subprogram parameter. Since they participate in the flow of information between variables, constants with variable inputs are treated like variables: they are part of a package’s state, and they must be listed in its state refinement whenever they are not visible. For example, constant Total_Min is not part of the state refinement of package Account below, while constant with variable inputs Total_Max is part of it:

package body Account with
  Refined_State => (State => (Total, Total_Max))
is
   Total     : Integer;
   Total_Min : constant Integer := 0;
   Total_Max : constant Integer := Compute_Total_Max(...);
   ...
end Account;

Global variables are not always the only constituents of a package’s state. For example, if a package P contains a nested package N, then N’s state is part of P’s state. As a consequence, if N is hidden, then its state must be listed in P’s refinement. For example, we can nest Account in the body of the Account_Manager package as follows:

package Account_Manager with
  Abstract_State => State
is
   ...
end Account_Manager;

package body Account_Manager with
  Refined_State => (State => Account.State)
is
   package Account with
     Abstract_State => State
   is
      ...
   end Account;
   ...
end Account_Manager;

5.3.1.3. State In The Private Part

Global variables and nested packages which themselves contain state may be declared in the private part of a package. For each such global variable and nested package state, it is mandatory to identify, using aspect Part_Of, the abstract state of the enclosing package of which it is a constituent:

package Account_Manager with
  Abstract_State => (Totals, Details)
is
   ...
private
   Total_Accounts : Integer with Part_Of => Totals;

   package Account with
     Abstract_State => (State with Part_Of => Details)
   is
      Total : Integer with Part_Of => Totals;
      ...
   end Account;
   ...
end Account_Manager;

The purpose of using Part_Of is to enforce that each constituent of an abstract state is known at the declaration of the constituent (not having to look at the package body), which is useful for both code understanding and tool analysis (including compilation).

As the state of a private child package is logically part of its parent package, aspect Part_Of must also be specified in that case:

private package Account_Manager.Account with
  Abstract_State => (State with Part_Of => Details)
is
   Total : Integer with Part_Of => Totals;
   ...
end Account_Manager.Account;

Aspect Part_Of can also be specified on a generic package instantiation inside a private part, to specify that all the state (visible global variables and abstract states) of the package instantiation is a constituent of an abstract state of the enclosing package:

package Account_Manager with
  Abstract_State => (Totals, Details)
is
   ...
private
   package Account is new Generic_Account (Max_Total) with Part_Of => Details;
   ...
end Account_Manager;

5.3.2. Package Initialization

[SPARK]

The package initialization specifies which global data (global variables, constant with variable inputs, and abstract state) defined in the package is initialized at package startup. The corresponding global variables may either be initialized at declaration, or by the package body statements. Thus, package initialization can be seen as the output data dependencies of the package elaboration procedure generated by the compiler.

For example, we can specify that the state of package Account is initialized at package startup as follows:

package Account with
  Abstract_State => State,
  Initializes    => State
is
   ...
end Account;

Then, unless Account’s implementation is not in SPARK, it should initialize the corresponding global variable Total either at declaration:

package body Account with
  Refined_State => (State => Total)
is
   Total : Integer := 0;
   ...
end Account;

or in the package body statements:

package body Account with
  Refined_State => (State => Total)
is
   Total : Integer;
   ...
begin
   Total := 0;
end Account;

These initializations need not correspond to direct assignments, but may be performed in a call, for example here to procedure Init_Total as seen in State Abstraction and Dependencies. A mix of initializations at declaration and in package body statements is also possible.

Package initializations also serve as dependency contracts for global variables’ initial values. That is, if the initial value of a global variable, state abstraction, or constant with variable inputs listed in a package initialization depends on the value of a variable defined outside the package, then this dependency must be listed in the package’s initialization. For example, we can initialize Total by reading the value of an external variable:

package Account with
  Abstract_State => State,
  Initializes    => (State => External_Variable)
is
   ...
end Account;

package body Account with
  Refined_State => (State => Total)
is
   Total : Integer := External_Variable;
   ...
end Account;

5.3.3. Package Initial Condition

[SPARK]

The package initial condition specifies the properties holding after package startup. Thus, package initial condition can be seen as the postcondition of the package elaboration procedure generated by the compiler. For example, we can specify that the value of Total defined in package Account’s implementation is initially zero:

package Account with
  Abstract_State    => State,
  Initial_Condition => Get_Total = 0
is
   function Get_Total return Integer;
   ...
end Account;

This is ensured either by initializing Total with value zero at declaration, or by assigning the value zero to Total in the package body statements, as seen in Package Initialization.

When the program is compiled with assertions (for example with switch -gnata in GNAT), the initial condition of a package is checked at run time after package startup. An exception is raised if the initial condition fails.

When a package is analyzed with GNATprove, it checks that the initial condition of a package cannot fail. GNATprove also analyzes the initial condition expression to ensure that it is free from run-time errors, like any other assertion.

5.3.4. Interfaces to the Physical World

[SPARK]

5.3.4.1. Volatile Variables

Most embedded programs interact with the physical world or other programs through so-called volatile variables, which are identified as volatile to protect them from the usual compiler optimizations. In SPARK, volatile variables are also analyzed specially, so that possible changes to their value from outside the program are taken into account, and so that changes to their value from inside the program are also interpreted correctly (in particular for checking flow dependencies).

For example, consider package Volatile_Or_Not which defines a volatile variable V and a non-volatile variable N, and procedure Swap_Then_Zero which starts by swapping the values of V and N before zeroing them out:

 1package Volatile_Or_Not with
 2  SPARK_Mode,
 3  Initializes => V
 4is
 5   V : Integer with Volatile;
 6   N : Integer;
 7
 8   procedure Swap_Then_Zero with
 9     Global  => (In_Out => (N, V)),
10     Depends => (V => N, N => null, null => V);
11
12end Volatile_Or_Not;
 1package body Volatile_Or_Not with
 2  SPARK_Mode
 3is
 4   procedure Swap_Then_Zero is
 5      Tmp : constant Integer := V;
 6   begin
 7      --  Swap values of V and N
 8      V := N;
 9      N := Tmp;
10      --  Zero out values of V and N
11      V := 0;
12      N := 0;
13   end Swap_Then_Zero;
14
15end Volatile_Or_Not;

Compare the difference in contracts between volatile variable V and non-volatile variable N:

  • The Package Initialization of package Volatile_Or_Not mentions V although this variable is not initialized at declaration or in the package body statements. This is because a volatile variable is assumed to be initialized.

  • The Flow Dependencies of procedure Swap_Then_Zero are very different for V and N. If both variables were not volatile, the correct contract would state that both input values are not used with null => (V, N) and that both output values depend on no inputs with (V, N) => null. The difference lies with the special treatment of volatile variable V: as its value may be read at any time, the intermediate value N assigned to V on line 8 of volatile_or_not.adb needs to be mentioned in the flow dependencies for output V.

GNATprove checks that Volatile_Or_Not and Swap_Then_Zero implement their contract, and it issues a warning on the first assignment to N:


volatile_or_not.adb:9:09: warning: unused assignment
    9 |      N := Tmp;
      |      ~~^~~~~~

This warning points to a real issue, as the intermediate value of N is not used before N is zeroed out on line 12. But note that no warning is issued on the similar first assignment to V, because the intermediate value of V may be read outside the program before V is zeroed out on line 11.

Note that in real code, the memory address of the volatile variable is set through aspect Address or the corresponding representation clause, so that it can be read or written outside the program.

5.3.4.2. Properties of Volatile Variables

Not all volatile variables are read and written outside the program, sometimes they are only read or only written outside the program. For example, the log introduced in State Abstraction could be implemented as an output port for the program logging the information, and as an input port for the program performing the logging. Two aspects are defined in SPARK to distinguish these different properties of volatile variables:

  • Aspect Async_Writers indicates that the value of the variable may be changed at any time (asynchronously) by hardware or software outside the program.

  • Aspect Async_Readers indicates that the value of the variable may be read at any time (asynchronously) by hardware or software outside the program.

Aspect Async_Writers has an effect on GNATprove’s proof: two successive reads of such a variable may return different results. Aspect Async_Readers has an effect on GNATprove’s flow analysis: an assignment to such a variable always has a potential effect, even if the value is never read in the program, since an external reader might actually read the value assigned.

These aspects are well suited to model respectively a sensor and a display, but not an input stream or an actuator, for which the act of reading or writing has an effect that should be reflected in the flow dependencies. Two more aspects are defined in SPARK to further refine the previous properties of volatile variables:

  • Aspect Effective_Reads indicates that reading the value of the variable has an effect (for example, removing a value from an input stream). It can only be specified on a variable that also has Async_Writers set.

  • Aspect Effective_Writes indicates that writing the value of the variable has an effect (for example, sending a command to an actuator). It can only be specified on a variable that also has Async_Readers set.

Both aspects Effective_Reads and Effective_Writes have an effect on GNATprove’s flow analysis: reading the former or writing the latter is modelled as having an effect on the value of the variable, which needs to be reflected in flow dependencies. Because reading a variable with Effective_Reads set has an effect on its value, such a variable cannot be only a subprogram input, it must be also an output.

For example, the program writing in a log each value passed as argument to procedure Add_To_Total may model the output port Log_Out as a volatile variable with Async_Readers and Effective_Writes set:

 1package Logging_Out with
 2  SPARK_Mode
 3is
 4   Total   : Integer;
 5   Log_Out : Integer with Volatile, Async_Readers, Effective_Writes;
 6
 7   procedure Add_To_Total (Incr : in Integer) with
 8     Global  => (In_Out => Total, Output => Log_Out),
 9     Depends => (Total =>+ Incr, Log_Out => Incr);
10
11end Logging_Out;
 1package body Logging_Out with
 2  SPARK_Mode
 3is
 4   procedure Add_To_Total (Incr : in Integer) is
 5   begin
 6      Total := Total + Incr;
 7      Log_Out := Incr;
 8   end Add_To_Total;
 9
10end Logging_Out;

while the logging program may model the input port Log_In as a volatile variable with Async_Writers and Effective_Reads set:

 1package Logging_In with
 2  SPARK_Mode
 3is
 4   Log_In : Integer with Volatile, Async_Writers, Effective_Reads;
 5
 6   type Integer_Array is array (Positive range 1 .. 100) of Integer;
 7   Log      : Integer_Array;
 8   Log_Size : Natural;
 9
10   procedure Get with
11     Global  => (In_Out => (Log, Log_Size, Log_In)),
12     Depends => ((Log_Size, Log_In) =>+ null, Log =>+ (Log_Size, Log_In));
13
14end Logging_In;
 1package body Logging_In with
 2  SPARK_Mode
 3is
 4   procedure Get is
 5   begin
 6      Log_Size := Log_Size + 1;
 7      Log (Log_Size) := Log_In;
 8   end Get;
 9
10end Logging_In;

GNATprove checks the specified data and flow dependencies on both programs.

A volatile variable on which none of the four aspects Async_Writers, Async_Readers, Effective_Reads or Effective_Writes is set is assumed to have all four aspects set to True. A volatile variable on which some of the four aspects are set to True is assumed to have the remaining ones set to False. See SPARK RM 7.1.3 for details.

5.3.4.3. Properties of Volatile Types

The four aspects Async_Writers, Async_Readers, Effective_Reads and Effective_Writes can be specified for a volatile type as well as a volatile variable. The rules stated for variables apply also to types for deciding on the value of the four aspects, when none, one or more values are specified explicitly. These aspects can only be specified on a type declaration, not on a subtype declaration.

Thus the declaration:

type T is new Integer;
Log_In : T with Volatile, Async_Writers, Effective_Reads;

can be written equivalently:

type T is new Integer with Volatile, Async_Writers, Effective_Reads;
Log_In : T;

5.3.4.4. Initialization of Volatile Variables and Variables with Address Clauses

For volatile variables and imported variables with address clauses, GNATprove assumes that the object is initialized. The following code does not raise errors about access to uninitialized data, and is proved. It does, however, raise several warnings on the object Y with an address clause, as it is not a precisely supported address clause.

X : Natural with Volatile;

subtype Even is Natural with Predicate => Even mod 2 = 0;

procedure Volatile_Init is
   Y : Even with Address => System'To_Address (16#DEADBEAF#), Import;
   Tmp : Integer := X;
begin
   pragma Assert (Y mod 2 = 0);
end P;

5.3.4.5. External State Abstraction

Volatile variables may be part of State Abstraction, in which case the volatility of the abstract name must be specified by using aspect External on the abstract name, as follows:

package Account with
  Abstract_State => (State with External)
is
   ...
end Account;

An external state may represent both volatile variables and non-volatile ones, for example:

package body Account with
  Refined_State => (State => (Total, Log, Log_Size))
is
   Total    : Integer;
   Log      : Integer_Array with Volatile;
   Log_Size : Natural with Volatile;
   ...
end Account;

The different Properties of Volatile Variables may also be specified in the state abstraction, which is then used by GNATprove to refine the analysis. For example, the program writing in a log seen in the previous section can be rewritten to abstract global variables as follows:

 1package Logging_Out_Abstract with
 2  SPARK_Mode,
 3  Abstract_State => (State with External => (Async_Readers, Effective_Writes)),
 4  Initializes => State
 5is
 6   procedure Add_To_Total (Incr : in Integer) with
 7     Global  => (In_Out => State),
 8     Depends => (State =>+ Incr);
 9
10end Logging_Out_Abstract;
 1package body Logging_Out_Abstract with
 2  SPARK_Mode,
 3  Refined_State => (State => (Log_Out, Total))
 4is
 5   Total   : Integer := 0;
 6   Log_Out : Integer := 0 with Volatile, Async_Readers, Effective_Writes;
 7
 8   procedure Add_To_Total (Incr : in Integer) with
 9     Refined_Global  => (In_Out => Total, Output => Log_Out),
10     Refined_Depends => (Total =>+ Incr, Log_Out => Incr)
11   is
12   begin
13      Total := Total + Incr;
14      Log_Out := Incr;
15   end Add_To_Total;
16
17end Logging_Out_Abstract;

while the logging program seen in the previous section may be rewritten to abstract global variables as follows:

1package Logging_In_Abstract with
2  SPARK_Mode,
3  Abstract_State => (State with External => (Async_Writers, Effective_Reads))
4is
5   procedure Get with
6     Global  => (In_Out => State),
7     Depends => (State =>+ null);
8
9end Logging_In_Abstract;
 1package body Logging_In_Abstract with
 2  SPARK_Mode,
 3  Refined_State => (State => (Log_In, Log, Log_Size))
 4is
 5   Log_In : Integer with Volatile, Async_Writers, Effective_Reads;
 6
 7   type Integer_Array is array (Positive range 1 .. 100) of Integer;
 8   Log      : Integer_Array := (others => 0);
 9   Log_Size : Natural := 0;
10
11   procedure Get with
12     Refined_Global  => (In_Out => (Log, Log_Size, Log_In)),
13     Refined_Depends => ((Log_Size, Log_In) =>+ null, Log =>+ (Log_Size, Log_In))
14   is
15   begin
16      Log_Size := Log_Size + 1;
17      Log (Log_Size) := Log_In;
18   end Get;
19
20end Logging_In_Abstract;

GNATprove checks the specified data and flow dependencies on both programs.

An external abstract state on which none of the four aspects Async_Writers, Async_Readers, Effective_Reads or Effective_Writes is set is assumed to have all four aspects set to True. An external abstract state on which some of the four aspects are set to True is assumed to have the remaining ones set to False. See SPARK RM 7.1.2 for details.