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:
No value of
SPARK_Mode
is specified as a configuration pragma. In that case, only the parts of the program explicitly marked withSPARK_Mode => On
are in SPARK. This default is recommended if only a small number of units or subprograms are in SPARK.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 withSPARK_Mode => Off
or a configuration pragma ofAuto
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 specimmediately following the
begin
keyword of a library-level package bodyimmediately 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 specimmediately 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:
the package public declarations
the package private part
the body of the package
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:
the spec
the private part
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;