SPARK Overview
This tutorial is an introduction to the SPARK programming language and its formal verification tools. You need not know any specific programming language (although going over the Introduction to Ada course first may help) or have experience in formal verification.
For some of the sample code presented, you'll be able to compile and run the program and/or run the formal verification tool on the program. These are available through the buttons labelled:
Run: compile the code with assertions enabled and run the executable produced.
Examine: perform the flow analysis stage of formal verification
Prove: perform the proof stage of formal verification (which includes flow analysis)
You can edit the sample code, so you can modify it and rerun the tools to see the effect of your changes on the compilation or analysis. Use the Reset button to restore the example to its initial version.
What is it?
SPARK refers to two different things:
a programming language targeted at functional specification and static verification, and
a set of development and verification tools for that language.
The SPARK language is based on a subset of the Ada language. Ada is particularly well suited to formal verification since it was designed for critical software development. SPARK builds on that foundation.

Version 2012 of Ada introduced the use of aspects, which can be used for subprogram contracts, and version 2014 of SPARK added its own aspects to further aid static analysis.
What do the tools do?
We start by reviewing static verification of programs, which is verification of the source code performed without compiling or executing it. Verification uses tools that perform static analysis. These can take various forms. They include tools that check types and enforce visibility rules, such as the compiler, in addition to those that perform more complex reasoning, such as abstract interpretation, as done by a tool like CodePeer from AdaCore. The tools that come with SPARK perform two different forms of static analysis:
flow analysis is the fastest form of analysis. It checks initializations of variables and looks at data dependencies between inputs and outputs of subprograms. It can also find unused assignments and unmodified variables.
proof checks for the absence of runtime errors as well as the conformance of the program with its specifications.
Key Tools
The tool for formal verification of the SPARK language is called GNATprove. It checks for conformance with the SPARK subset and performs flow analysis and proof of the source code. Several other tools support the SPARK language, including both the GNAT compiler and the GNAT Studio integrated development environment.
A trivial example
We start with a simple example of a subprogram in Ada that uses SPARK
aspects to specify verifiable subprogram contracts. The subprogram, called
Increment
, adds 1 to the value of its parameter X
:
The contracts are written using the Ada aspect feature and those shown specify several properties of this subprogram:
The SPARK Global aspect says that
Increment
does not read or write any global variables.The SPARK Depend aspect is especially interesting for security: it says that the value of the parameter
X
after the call depends only on the (previous) value ofX
.The
Pre
andPost
aspects of Ada specify functional properties ofIncrement
:Increment
is only allowed to be called if the value ofX
prior to the call is less thanInteger'Last
. This ensures that the addition operation performed in the subprogram body doesn't overflow.Increment
does indeed perform an increment ofX
: the value ofX
after a call is one greater than its value before the call.
GNATprove can verify all of these contracts. In addition, it verifies
that no error can be raised at runtime when executing Increment
's
body.
The Programming Language
It's important to understand why there are differences between the SPARK and Ada languages. The aim when designing the SPARK subset of Ada was to create the largest possible subset of Ada that was still amenable to simple specification and sound verification.
The most notable restrictions from Ada are related to exceptions and access types, both of which are known to considerably increase the amount of user-written annotations required for full support. Backwards goto statements and controlled types are also not supported since they introduce non-trivial control flow. The two remaining restrictions relate to side-effects in expressions and aliasing of names, which we now cover in more detail.
Limitations
No side-effects in expressions
The SPARK language doesn't allow side-effects in expressions. In other
words, evaluating a SPARK expression must not update any object. This
limitation is necessary to avoid unpredictable behavior that depends on
order of evaluation, parameter passing mechanisms, or compiler
optimizations. The expression for Dummy
below is non-deterministic due to
the order in which the two calls to F are evaluated. It's therefore not
legal SPARK.
In fact, the code above is not even legal Ada, so the same error is generated by the GNAT compiler. But SPARK goes further and GNATprove also produces an error for the following equivalent code that is accepted by the Ada compiler:
The SPARK languages enforces the lack of side-effects in expressions by
forbidding side-effects in functions, which include modifications to either
parameters or global variables. As a consequence, SPARK forbids functions
with out
or in out
parameters in addition to functions
modifying a global variable. Function F
below is illegal in
SPARK, while Function Incr
might be legal if it doesn't modify any
global variables and function Incr_And_Log
might be illegal if it
modifies global variables to perform logging.
function F (X : in out Integer) return Integer; -- Illegal
function Incr (X : Integer) return Integer; -- OK?
function Incr_And_Log (X : Integer) return Integer; -- OK?
In most cases, you can easily replace these functions by procedures with an
out
parameter that returns the computed value.
When it has access to function bodies, GNATprove verifies that those
functions are indeed free from side-effects. Here for example, the two
functions Incr
and Incr_And_Log
have the same signature, but only
Incr
is legal in SPARK. Incr_And_Log
isn't: it attempts to update
the global variable Call_Count
.
No aliasing of names
Another restriction imposed by the SPARK subset concerns aliasing. We say that two names are aliased if they refer to the same object. There are two reasons why aliasing is forbidden in SPARK:
It makes verification more difficult because it requires taking into account the fact that modifications to variables with different names may actually update the same object.
Results may seem unexpected from a user point of view. The results of a subprogram call may depend on compiler-specific attributes, such as parameter passing mechanisms, when its parameters are aliased.
Aliasing can occur as part of the parameter
passing that occurs in a subprogram call. Functions have no side-effects in
SPARK, so aliasing of parameters in function calls isn't problematic; we
need only consider procedure calls. When a procedure is called, SPARK
verifies that no out
or in out
parameter is aliased with
either another parameter of the procedure or a global variable modified in
the procedure's body.
Procedure Move_To_Total
is an example where the possibility of aliasing
wasn't taken into account by the programmer:
Move_To_Total
adds the value of its input parameter Source
to
the global variable Total
and then resets Source
to 0. The
programmer has clearly not taken into account the possibility of an
aliasing between Total
and Source
. (This sort of error is
quite common.)
This procedure itself is valid SPARK. When doing verification,
GNATprove assumes, like the programmer did, that there's no aliasing
between Total
and Source
. To ensure this assumption is valid,
GNATprove checks for possible aliasing on every call to
Move_To_Total
. Its final call in procedure No_Aliasing
violates this assumption, which produces both a message from GNATprove
and a runtime error (an assertion violation corresponding to the
expected change in Total
from calling Move_To_Total
). Note
that the postcondition of Move_To_Total
is not violated on this
second call since integer parameters are passed by copy and the
postcondition is checked before the copy-back from the formal
parameters to the actual arguments.
Aliasing can also occur as a result of using access types (pointers in Ada). These are restricted in SPARK so that only benign aliasing is allowed, when both names are only used to read the data. In particular, assignment between access objects operates a transfer of ownership, where the source object loses its permission to read or write the underlying allocated memory.
Procedure Ownership_Transfer
is an example of code that is legal in Ada but
rejected in SPARK due to aliasing:
After the assignment of X
to Y
, variable X
cannot be used anymore
to read or write the underlying allocated memory.
Note
For more details on these limitations, see the SPARK User's Guide.
Designating SPARK Code
Since the SPARK language is restricted to only allow easily specifiable and verifiable constructs, there are times when you can't or don't want to abide by these limitations over your entire code base. Therefore, the SPARK tools only check conformance to the SPARK subset on code which you identify as being in SPARK.
You do this by using an aspect named SPARK_Mode
. If you don't
explicitly specify otherwise, SPARK_Mode
is Off, meaning you can
use the complete set of Ada features in that code and that it should not be
analyzed by GNATprove. You can change this default either selectively (on
some units or subprograms or packages inside units) or globally (using a
configuration pragma, which is what we're doing in this tutorial). To allow
simple reuse of existing Ada libraries, entities declared in imported units
with no explicit SPARK_Mode
can still be used from SPARK code. The
tool only checks for SPARK conformance on the declaration of those entities
which are actually used within the SPARK code.
Here's a common case of using the SPARK_Mode
aspect:
package P
with SPARK_Mode => On
is
-- package spec is IN SPARK, so can be used by SPARK clients
end P;
package body P
with SPARK_Mode => Off
is
-- body is NOT IN SPARK, so is ignored by GNATprove
end P;
The package P
only defines entities whose specifications are in the
SPARK subset. However, it wants to use all Ada features in its body.
Therefore the body should not be analyzed and has its SPARK_Mode
aspect set to Off.
You can specify SPARK_Mode
in a fine-grained manner on a per-unit
basis. An Ada package has four different components: the visible and
private parts of its specification and the declarative and statement parts
of its body. You can specify SPARK_Mode
as being either On or
Off on any of those parts. Likewise, a subprogram has two parts: its
specification and its body.
A general rule in SPARK is that once SPARK_Mode
has been set to
Off, it can never be switched On again in the same part of a package or
subprogram. This prevents setting SPARK_Mode
to On for subunits of
a unit with SPARK_Mode
Off and switching back to SPARK_Mode
On for a part of a given unit where it was set fo Off in a previous
part.
Note
For more details on the use of SPARK_Mode
, see the
SPARK User's Guide.
Code Examples / Pitfalls
Example #1
Here's a package defining an abstract stack type (defined as a private type
in SPARK) of Element
objects along with some subprograms providing the
usual functionalities of stacks. It's marked as being in the SPARK subset.
Side-effects in expressions are not allowed in SPARK. Therefore, Pop
is not allowed to modify its parameter S
.
Example #2
Let's turn to an abstract state machine version of a stack, where the unit
provides a single instance of a stack. The content of the stack (global
variables Content
and Top
) is not directly visible to clients. In
this stripped-down version, only the function Pop
is available to
clients. The package spec and body are marked as being in the SPARK subset.
As above, functions should be free from side-effects. Here, Pop
updates
the global variable Top
, which is not allowed in SPARK.
Example #3
We now consider two procedures: Permute
and Swap
. Permute
applies a circular permutation to the value of its three parameters.
Swap
then uses Permute
to swap the value of X
and Y
.
Here, the values for parameters Y
and Z
are aliased in the call to
Permute
, which is not allowed in SPARK. In fact, in this particular
case, this is even a violation of Ada rules so the same error is issued by
the Ada compiler.
In this example, we see the reason why aliasing is not allowed in SPARK:
since Y
and Z
are Positive
, they are passed by copy and the
result of the call to Permute
depends on the order in which they're
copied back after the call.
Example #4
Here, the Swap
procedure is used to swap the value of the two record
components of R
.
This code is correct. The call to Swap
is safe: two different
components of the same record can't refer to the same object.
Example #5
Here's a slight modification of the previous example using an array instead
of a record: Swap_Indexes
calls Swap
on values stored in the array
A
.
GNATprove detects a possible case of aliasing. Unlike the previous example,
it has no way of knowing that the two elements A (I)
and A (J)
are
actually distinct when we call Swap
. GNATprove issues a check message
here instead of an error, giving you the possibility of justifying the
message after review (meaning that you've verified manually that this
can't, in fact, occur).
Example #6
We now consider a package declaring a type Dictionary
, an array
containing a word per letter. The procedure Store
allows us to insert a
word at the correct index in a dictionary.
This code is not correct: controlled types are not part of the SPARK
subset. The solution here is to use SPARK_Mode
to separate the
definition of String_Access
from the rest of the code in a fine
grained manner.
Example #7
Here's a new version of the previous example, which we've modified to hide the
controlled type inside the private part of package P
, using pragma
SPARK_Mode (Off)
at the start of the private part.
Since the controlled type is defined and used inside of a part of the code ignored by GNATprove, this code is correct.
Example #8
Let's put together the new spec for package P
with the body of P
seen
previously.
The body of Store
doesn't actually use any construct that's not in the
SPARK subset, but we nevertheless can't set SPARK_Mode
to On
for
P
's body because it has visibility to P
's private part, which is
not in SPARK, even if we don't use it.
Example #9
Next, we moved the declaration and the body of the procedure Store
to
another package named Q
.
And now everything is fine: we've managed to retain the use of the controlled type while having most of our code in the SPARK subset so GNATprove is able to analyze it.
Example #10
Our final example is a package with two functions to search for the value 0
inside an array A
. The first raises an exception if 0 isn't found in
A
while the other simply returns 0 in that case.
This code is perfectly correct, despite the use of exception handling,
because we've carefully isolated this non-SPARK feature in a function body
marked with a SPARK_Mode
of Off
so it's ignored by GNATprove.
However, GNATprove tries to show that Not_Found
is never raised in
Search_Zero_P
, producing a message about a possible exception being
raised. Looking at Search_Zero_N
, it's indeed likely that an exception
is meant to be raised in some cases, which means you need to verify that
Not_Found
is only raised when appropriate using other methods such as
peer review or testing.