This tutorial is an interactive 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 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.
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 GPS 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
The contracts are written using the Ada aspect feature and those shown specify several properties of this subprogram:
The SPARK Global aspect says that
Incrementdoes not read or write any global variables.
The SPARK Depend aspect is especially interesting for security: it says that the value of the parameter
Xafter the call depends only on the (previous) value of
Postaspects of Ada specify functional properties of
Incrementis only allowed to be called if the value of
Xprior to the call is less than
Integer'Last. This ensures that the addition operation performed in the subprogram body doesn't overflow.
Incrementdoes indeed perform an increment of
X: the value of
Xafter 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
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 exclusions from Ada include exceptions and access types (including related features such as allocators), both of which are known to considerably increase the amount of user-written annotations required. 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.
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
G below is non-deterministic due to
the order in which the two calls to F are evaluated. It's therefore not
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
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
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
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.
Since access types (pointers in Ada)
are not allowed in SPARK, aliasing can only 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
in out parameter is aliased with
either another parameter of the procedure or a global variable modified in
the procedure's body.
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
the global variable
Total and then resets
Source to 0. The
programmer has clearly not taken into account the possibility of an
Source. (This sort of error is
This procedure itself is valid SPARK. When doing verification,
GNATprove assumes, like the programmer did, that there's no aliasing
Source. To ensure this assumption is valid,
GNATprove checks for possible aliasing on every call to
Move_To_Total. Its final call in procedure
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
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.
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
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;
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
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
On for a part of a given unit where it was set fo Off in a previous
Code Examples / Pitfalls¶
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,
is not allowed to modify its parameter
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
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,
the global variable
Top, which is not allowed in SPARK.
We now consider two procedures:
applies a circular permutation to the value of its three parameters.
Swap then uses
Permute to swap the value of
Here, the values for parameters
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:
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.
Swap procedure is used to swap the value of the two record
This code is correct. The call to
Swap is safe: two different
components of the same record can't refer to the same object.
Here's a slight modification of the previous example using an array instead
of a record:
Swap on values stored in the array
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).
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: access types are not part of the SPARK subset. In
this case, they are very useful because without them we can't store
arbitrarily long strings in an array. One solution here is to use
SPARK_Mode to separate parts of the access type from the rest of the
code in a fine grained manner.
Here's a new version of the previous example, which we've modified to hide
the access type inside the private part of package
SPARK_Mode (Off) at the start of the private part.
Since the access type is defined and used inside of a part of the code ignored by GNATprove, this code is correct.
Let's put together the new spec for package
P with the body of
The body of
Store doesn't actually use any construct that's not in the
SPARK subset, but we nevertheless can't set
P's body because it has visibility to
P's private part, which is
not in SPARK, even if we don't use it.
Next, we moved the declaration and the body of the procedure
another package named
And now everything is fine: we've managed to retain the use of the access type while having most of our code in the SPARK subset so GNATprove is able to analyze it.
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
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.