4. Identifying SPARK Code

In general a program can have some parts that are in SPARK (and follow all the rules in the SPARK Reference Manual), and some parts that are full Ada. Pragma or aspect SPARK_Mode is used to identify which parts are in SPARK (by default programs are in full Ada).

This section contains a simple description of pragma and aspect SPARK_Mode. See Aspect and Pragma SPARK_Mode for the complete description.

Note that GNATprove only analyzes parts of the code that are identified as being in SPARK using pragma or aspect SPARK_Mode.

4.1. Mixing SPARK Code and Ada Code

An Ada program unit or other construct is said to be “in SPARK” if it complies with the restrictions required to permit formal verification given in the SPARK Reference Manual. Conversely, an Ada program unit or other construct is “not in SPARK” if it does not meet these requirements, and so is not amenable to formal verification.

Within a single Ada unit, constructs which are “in” and “not in” SPARK may be mixed at a fine level in accordance with the following two general principles:

  • SPARK code shall only reference SPARK declarations, but a SPARK declaration which requires a completion may have a non-SPARK completion.

  • SPARK code may enclose non-SPARK code.

  • non-SPARK code may enclose SPARK code only at library level. A subprogram body which is not in SPARK cannot contain SPARK code.

More specifically, non-SPARK completions of SPARK declarations are allowed for subprogram declarations, package declarations, task type declarations, protected type declarations, private type declarations, private extension declarations, and deferred constant declarations. [Strictly speaking, the private part of a package, a task type or a protected type is considered to be part of its completion for purposes of the above rules; this is described in more detail below].

When a non-SPARK completion is provided for a SPARK declaration, the user has an obligation to ensure that the non-SPARK completion is consistent (with respect to the semantics of SPARK) with its SPARK declaration. For example, SPARK requires that a function call has no side effects. If the body of a given function is in SPARK, then this rule is enforced via various language rules; otherwise, it is the responsibility of the user to ensure that the function body does not violate this rule. As with other such constructs (notably pragma Assume), failure to meet this obligation can invalidate any or all analysis (proofs and/or flow analysis) associated with the SPARK portion of a program. A non-SPARK completion meets this obligation if it is semantically equivalent (with respect to dynamic semantics) to some notional completion that could have been written in SPARK.

When a non-SPARK package declaration or body is included in a SPARK subprogram or package, the user has an obligation to ensure that the non-SPARK declaration is consistent (with respect to the semantics of SPARK) with a hypothetical equivalent SPARK declaration. For example, SPARK requires that package elaboration code cannot modify variables defined outside of the package.

The SPARK semantics (specifically including flow analysis and proof) of a “mixed” program which meets the aforementioned requirement are well defined - they are the semantics of the equivalent 100% SPARK program. For the semantics of other “mixed” programs refer to the Ada Reference Manual.

In the case of a package, a task type, or a protected type, the specification/completion division described above is a simplification of the true situation. For instance, a package is divided into 4 sections, not just 2: its visible part, its private part, the declarations of its body, and the statement list of its body. For a given package and any number N in the range 0 .. 4, the first N sections of the package might be in SPARK while the remainder is not.

For example, the following combinations may be typical:

  • Package specification in SPARK. Package body not in SPARK.

  • Visible part of package specification in SPARK. Private part and body not in SPARK.

  • Package specification in SPARK. Package body almost entirely in SPARK, with a small number of subprogram bodies not in SPARK.

  • Package specification in SPARK, with all subprogram bodies imported from another language.

  • Package specification contains a mixture of declarations which are in SPARK and not in SPARK. The latter declarations are only visible and usable from client units which are not in SPARK.

Task types and protected types are similar to packages but only have 3 sections instead of 4. The statement list section of the body is missing.

Another typical use is to exempt part of a subprogram from analysis by isolating it in a local subprogram whose body is not in SPARK.

Such patterns are intended to allow for application of formal verification to a subset of a program, and the combination of formal verification with more traditional testing (see Applying SPARK in Practice).

4.2. Project File Setup

The project file is used to identify coarsely which parts of a program are in SPARK. To get more details on project file setup, see section Setting Up a Project File.

4.2.1. Setting the Default SPARK_Mode

There are two possible defaults:

  1. No value of SPARK_Mode is specified as a configuration pragma. In that case, only the parts of the program explicitly marked with SPARK_Mode => On are in SPARK. This default is recommended if only a small number of units or subprograms are in SPARK.

  2. A value of SPARK_Mode => On is specified as a configuration pragma. In that case, all the program should be in SPARK, except for those parts explicitly marked with SPARK_Mode => Off or a configuration pragma of Auto inside files. This mode is recommended if most of the program is in SPARK.

Here is how to specify a value of SPARK_Mode => On as a configuration pragma:

project My_Project is
   package Builder is
      for Global_Configuration_Pragmas use "spark.adc";
   end Builder;
end My_Project;

where spark.adc is a configuration file containing at least the following line:

pragma SPARK_Mode (On);

4.2.2. Specifying Files To Analyze

By default, all files from a project are analyzed by GNATprove. It may be useful to restrict the set of files to analyze to speedup analysis if only a subset of the files contain SPARK code.

The set of files to analyze can be identified by specifying a different value of various project attributes in the mode used for formal verification:

  • Source_Dirs: list of source directory names

  • Source_Files: list of source file names

  • Source_List_File: name of a file listing source file names

For example:

project My_Project is

  Mode := External ("GPR_TOOL", "");

  case Mode is
     when "gnatprove" =>
        for Source_Dirs use ("dir1", "dir2");
        for Source_Files use ("file1.ads", "file2.ads", "file1.adb", "file2.adb");
     when others =>
        for Source_Dirs use (...);
  end case;

  package Compiler is
     case Mode is
        when "gnatprove" =>
           for Switches ("Ada") use ...
        when others =>
           for Switches ("Ada") use ...
     end case;
  end Compiler;

end My_Project;

4.2.3. Excluding Files From Analysis

When choosing a default value of SPARK_Mode => On, it may be needed to exclude some files from analysis (for example, because they contain non-SPARK code, or code that does not need to be formally analyzed).

The set of files to exclude can be identified by specifying a different value of various project attributes in the mode used for formal verification:

  • Excluded_Source_Dirs: list of excluded source directory names

  • Excluded_Source_Files: list of excluded source file names

  • Excluded_Source_List_File: name of a file listing excluded source file names

For example:

project My_Project is
   package Builder is
      for Global_Configuration_Pragmas use "spark.adc";
   end Builder;

  Mode := External ("GPR_TOOL", "");

  case Mode is
     when "gnatprove" =>
        for Excluded_Source_Files use ("file1.ads", "file1.adb", "file2.adb");
     when others =>
        null;
  end case;

end My_Project;

4.2.4. Using Multiple Projects

Sometimes, it is more convenient to analyze a subset of the source files with the default SPARK_Mode => On and the rest of the source files with no setting for SPARK_Mode. In that case, one can use two project files with different defaults, with each source file in one of the projects only. Files in one project can still refer to files in the other project by using a limited with clause between projects, as follows:

limited with "project_b"
project My_Project_A is
   package Compiler is
      for Local_Configuration_Pragmas use "spark.adc";
   end Compiler;
   for Source_Files use ("file1.ads", "file2.ads", "file1.adb", "file2.adb");
end My_Project_A;

limited with "project_a"
project My_Project_B is
   for Source_Files use ("file3.ads", "file4.ads", "file3.adb", "file4.adb");
end My_Project_B;

where spark.adc is a configuration file containing at least the following line:

pragma SPARK_Mode (On);

4.3. Using SPARK_Mode in Code

The pragma or aspect SPARK_Mode can be used in the code to identify precisely which parts of a program are in SPARK.

4.3.1. Basic Usage

The form of a pragma SPARK_Mode is as follows:

pragma SPARK_Mode [ (Auto | On | Off) ]

For example:

pragma SPARK_Mode (On);
package P is

The value Auto is only allowed in configuration pragmas, either in a configuration pragma file, or inside a source file. Thus, value Auto is not allowed in aspect SPARK_Mode. Having a value Auto means that the file is analyzed as if no value of SPARK_Mode was specified, which is useful in cases where SPARK_Mode => On is specified in a configuration pragma file for the complete project, but a file contains both entities compatible with SPARK and entities not in SPARK.

The form of an aspect SPARK_Mode is as follows:

with SPARK_Mode => [ On | Off ]

For example:

package P with
  SPARK_Mode => On
is

A default argument of On is assumed for any SPARK_Mode pragma or aspect for which no argument is explicitly specified.

For example:

package P is
   pragma SPARK_Mode;  --  On is implicit here

or

package P with
  SPARK_Mode  --  On is implicit here
is

We say that a package or a subprogram is library-level if it is either top-level (i.e. it is a library unit; its declaration is the outermost program unit declared in a given compilation unit) or declared immediately within another library-level package (which excludes, for example, declarations inside subprogram bodies). For example, all the packages in the following code snippet are library-level packages:

package P is
   package Q is
      package R is
...
package body P is
   package S is
      package T is

The SPARK_Mode pragma can be used in the following places in the code:

  • as a configuration pragma at unit level (even before with-clauses) in particular for unit-level generic instantiations

  • immediately within a library-level package spec

  • immediately within a library-level package body

  • immediately following the private keyword of a library-level package spec

  • immediately following the begin keyword of a library-level package body

  • immediately following a library-level subprogram spec

  • immediately within a library-level subprogram body

  • immediately within a library-level task spec

  • immediately within a library-level task body

  • immediately following the private keyword of a library-level task spec

  • immediately within a library-level protected spec

  • immediately within a library-level protected body

  • immediately following the private keyword of a library-level protected spec

The SPARK_Mode aspect can be used in the following places in the code:

  • on a library-level package spec or body

  • on a library-level subprogram spec or body

  • on a library-level task spec or body

  • on a library-level protected spec or body

If a SPARK_Mode pragma or aspect is not specified for a subprogram, package, task or protected spec/body, then its value is inherited from the current mode that is active at the point where the declaration occurs.

Note that a generic package instance is considered to be declared at its instantiation point. For example, a generic package cannot be both marked SPARK_Mode and instantiated in a subprogram body.

4.3.2. Consistency Rules

The basic rule is that you cannot turn SPARK_Mode back On, once you have explicitly turned if Off. So the following rules apply:

If a subprogram spec has SPARK_Mode Off, then the body cannot have SPARK_Mode On.

For a package, we have four parts:

  1. the package public declarations

  2. the package private part

  3. the body of the package

  4. the elaboration code after begin

For a package, the rule is that if you explicitly turn SPARK_Mode Off for any part, then all the following parts cannot have SPARK_Mode On. Note that this may require repeating a pragma SPARK_Mode (Off) in the body. For example, if we have a configuration pragma SPARK_Mode (On) that turns the mode On by default everywhere, and one particular package spec has pragma SPARK_Mode (Off), then that pragma will need to be repeated in the package body.

Task types and protected types are handled similarly. If SPARK_Mode is set to Off on one part, it cannot be set to On on the following parts, among the three parts:

  1. the spec

  2. the private part

  3. the body

There is an exception to this rule, when SPARK_Mode occurs in the code of a generic instantiated in code where SPARK_Mode is Off. In that case, occurrences of SPARK_Mode in the generic are ignored for this instance.

4.3.3. Examples of Use

4.3.3.1. Verifying Selected Subprograms

If only a few selected subprograms are in SPARK, then it makes sense to set no default for SPARK_Mode, and instead set SPARK_Mode => On directly on the subprograms of interest. For example:

 1package Selected_Subprograms is
 2
 3   procedure Critical_Action with
 4     SPARK_Mode => On;
 5
 6   procedure Sub_Action (X : out Boolean) with
 7     Post => X = True;
 8
 9   procedure Non_Critical_Action;
10
11end Selected_Subprograms;

Note that, although the bodies of procedures Sub_Action and Non_Critical_Action are not analyzed, it is valid to call Sub_Action in the body of procedure Critical_Action, even without specifying SPARK_Mode => On on the spec of Sub_Action. Indeed, GNATprove checks in that case that the spec of Sub_Action is in SPARK.

 1package body Selected_Subprograms is
 2
 3   procedure Critical_Action with
 4     SPARK_Mode => On
 5   is
 6      --  this procedure body is analyzed
 7      X : Boolean;
 8   begin
 9      Sub_Action (X);
10      pragma Assert (X = True);
11   end Critical_Action;
12
13   procedure Sub_Action (X : out Boolean) is
14   begin
15      --  this procedure body is not analyzed
16      X := True;
17   end Sub_Action;
18
19   procedure Non_Critical_Action is
20   begin
21      --  this procedure body is not analyzed
22      null;
23   end Non_Critical_Action;
24
25end Selected_Subprograms;

4.3.3.2. Verifying Selected Units

If only a few selected units are in SPARK, then it makes sense to set no default for SPARK_Mode, and instead set SPARK_Mode => On directly on the units of interest. For example:

 1package Selected_Units with
 2  SPARK_Mode => On
 3is
 4
 5   procedure Critical_Action;
 6
 7   procedure Sub_Action (X : out Boolean) with
 8     Post => X = True;
 9
10   procedure Non_Critical_Action with
11     SPARK_Mode => Off;
12
13end Selected_Units;

Note that procedure Sub_Action can be called inside SPARK code, because its spec is in SPARK, even though its body is marked SPARK_Mode => Off. On the contrary, procedure Non_Critical_Action whose spec is marked SPARK_Mode => Off cannot be called inside SPARK code.

 1package body Selected_Units with
 2  SPARK_Mode => On
 3is
 4
 5   procedure Critical_Action is
 6      --  this procedure body is analyzed
 7      X : Boolean;
 8   begin
 9      Sub_Action (X);
10      pragma Assert (X = True);
11   end Critical_Action;
12
13   procedure Sub_Action (X : out Boolean) with
14     SPARK_Mode => Off
15   is
16   begin
17      --  this procedure body is not analyzed
18      X := True;
19   end Sub_Action;
20
21   procedure Non_Critical_Action with
22     SPARK_Mode => Off
23   is
24   begin
25      --  this procedure body is not analyzed
26      null;
27   end Non_Critical_Action;
28
29end Selected_Units;

4.3.3.3. Excluding Selected Unit Bodies

If a unit spec is in SPARK, but its body is not in SPARK, the spec can be marked with SPARK_Mode => On and the body with SPARK_Mode => Off. This allows client code in SPARK to use this unit. If SPARK_Mode is On by default, then it need not be repeated on the unit spec.

 1package body Exclude_Unit_Body with
 2  SPARK_Mode => Off
 3is
 4   --  this package body is not analyzed
 5
 6   Value : T := new Integer;
 7
 8   function Get_Value return Integer is
 9   begin
10      return Value.all;
11   end Get_Value;
12
13   procedure Set_Value (V : Integer) is
14   begin
15      Value.all := V;
16   end Set_Value;
17
18end Exclude_Unit_Body;

Note that the private part of the spec (which is physically in the spec file, but is logically part of the implementation) can be excluded as well, by using a pragma SPARK_Mode (Off) at the start of the private part.

 1package Exclude_Unit_Body with
 2  SPARK_Mode => On
 3is
 4
 5   type T is private;
 6
 7   function Get_Value return Integer;
 8
 9   procedure Set_Value (V : Integer) with
10     Post => Get_Value = V;
11
12private
13   pragma SPARK_Mode (Off);
14
15   --  the private part of the package spec is not analyzed
16
17   type T is access Integer;
18end Exclude_Unit_Body;

This scheme also works on generic units, which can then be instantiated both in code where SPARK_Mode is On, in which case only the body of the instantiated generic is excluded, or in code where SPARK_Mode is Off, in which case both the spec and the body of the instantiated generic are excluded.

1generic
2   type T is private;
3package Exclude_Generic_Unit_Body with
4  SPARK_Mode => On
5is
6   procedure Process (X : in out T);
7end Exclude_Generic_Unit_Body;

1package body Exclude_Generic_Unit_Body with
2  SPARK_Mode => Off
3is
4   --  this package body is not analyzed
5   procedure Process (X : in out T) is
6   begin
7      null;
8   end Process;
9end Exclude_Generic_Unit_Body;

 1with Exclude_Generic_Unit_Body;
 2pragma Elaborate_All (Exclude_Generic_Unit_Body);
 3
 4package Use_Generic with
 5  SPARK_Mode => On
 6is
 7   --  the spec of this generic instance is analyzed
 8   package G1 is new Exclude_Generic_Unit_Body (Integer);
 9
10   procedure Do_Nothing;
11
12end Use_Generic;

 1package body Use_Generic with
 2  SPARK_Mode => Off
 3is
 4   type T is access Integer;
 5
 6   --  this generic instance is not analyzed
 7   package G2 is new Exclude_Generic_Unit_Body (T);
 8
 9   procedure Do_Nothing is
10   begin
11      null;
12   end Do_Nothing;
13
14end Use_Generic;

4.3.3.4. Excluding Selected Parts of a Unit

If most units are in SPARK except from some subprograms and packages, it makes sense to set the default to SPARK_Mode (On), and set SPARK_Mode => Off on non-SPARK declarations. We assume here that a value of SPARK_Mode => On is specified as a configuration pragma.

 1package Exclude_Selected_Parts is
 2
 3   procedure Critical_Action;
 4
 5   procedure Non_Critical_Action;
 6
 7   package Non_Critical_Data with
 8     SPARK_Mode => Off
 9   is
10      type T is access Integer;
11      X : T;
12      function Get_X return Integer;
13   end Non_Critical_Data;
14
15end Exclude_Selected_Parts;

Note that procedure Non_Critical_Action can be called inside SPARK code, because its spec is in SPARK, even though its body is marked SPARK_Mode => Off.

Note also that the local package Non_Critical_Data can contain any non-SPARK types, variables and subprograms, as it is marked SPARK_Mode => Off. It may be convenient to define such a local package to gather non-SPARK declarations, which allows to mark globally the unit Exclude_Selected_Parts with SPARK_Mode => On.

 1package body Exclude_Selected_Parts is
 2
 3   procedure Critical_Action is
 4   begin
 5      --  this procedure body is analyzed
 6      Non_Critical_Action;
 7   end Critical_Action;
 8
 9   procedure Non_Critical_Action with
10     SPARK_Mode => Off
11   is
12   begin
13      --  this procedure body is not analyzed
14      null;
15   end Non_Critical_Action;
16
17   package body Non_Critical_Data with
18     SPARK_Mode => Off
19   is
20      --  this package body is not analyzed
21      function Get_X return Integer is
22      begin
23         return X.all;
24      end Get_X;
25   end Non_Critical_Data;
26
27end Exclude_Selected_Parts;