This tutorial is an interactive introduction to the SPARK programming language and formal verification tools. It does not require you to know any specific programming language (although going over the Introduction to Ada first may help) or to have experience in formal verification.
For some of the code snippets presented, you will 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 just produced.
- Examine: perform the flow analysis stage of formal verification
- Prove: perform the proof stage of formal verification (which includes flow analysis)
These code snippets are editable, so you can modify the code and rerun the tools to see the effect on compilation or analysis. Use the button Reset to restore the initial version of the example.
What is it?¶
SPARK refers to two different things:
- a programming language targeted at functional specification and static verification, plus
- a set of development and verification tools.
The SPARK language is based on a subset of the Ada language, which is particularly suited to formal verification, as it is designed for critical software development.
Version 2012 of Ada introduced the use of aspects that can be used for subprogram contracts, and version 2014 of SPARK added its own aspects in order to aid static analysis.
What do the tools do?¶
We shall start by reviewing static verification of your programs, meaning the verification of the source code directly without compiling or executing it. This verification involves tools that perform static analysis and this, in general, can take various forms. It includes, for example, type checking and visibility rules enforcement, as done by the compiler, as well as 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:
- The first one is called flow analysis and, in general, it is the fastest form of analysis. It checks in particular initialization of variables and data dependencies between inputs and outputs of subprograms. It can also find unused assignments and unmodified variables.
- The second one is called proof and it checks in particular absence of runtime errors in program execution as well as conformance with 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. The SPARK language is also supported by several other tools. In particular, it is fully supported by the GNAT compiler and by the GPS integrated development environment.
A trivial example¶
We will now look at a simple example of subprogram in Ada that also uses
SPARK aspects to specify a verifiable subprogram contract. The subprogram
Increment adds 1 to the value of its parameter
Several properties are specified on this subprogram using the contracts shown:
The SPARK Global aspect specifies that
Incrementdoes not read and does not write any global variable.
The SPARK Depend aspect is especially interesting for security, as it specifies that the value of the parameter
Xafter the call only depends on the value of
Xbefore the call.
Functional properties of Increment are specified using the
Postaspects of Ada.
- Increment can only be called if the value of
Xbefore the call is smaller that
Integer'Last. It is necessary to ensure that the addition operation performed in the subprogram body will also not overflow.
- Finally, we specify that
Incrementdoes indeed perform an increment of
X, that is, the value of
Xafter a call is one more than its value before the call.
- Increment can only be called if the value of
GNATprove can verify all of these contracts. It additionally makes sure that no
error may be raised at runtime when executing
The Programming Language¶
At this point it helps to understand the rationale behind the differences between the SPARK and Ada languages. The aim while designing the SPARK subset of Ada was to create the biggest possible subset still amenable to easy specification and sound verification.
The most notable exclusions include access types and allocators, as well as handling of exceptions, which are both known to increase considerably the amount of required user-written annotations. Goto statements and controlled types are also not supported as they introduce non-trivial control flow. The two remaining restrictions are side-effects in expressions and aliasing of names, which we will now look at in more detail.
No side-effects in expressions¶
The SPARK language does not support side-effects in expressions, that is,
evaluating a SPARK expression cannot update any object. This limitation is
necessary to avoid unpredictable behavior depending on order of
evaluation, parameter passing mechanism, or compiler optimizations. The
expression below for
G is non-deterministic due to the order in which
the two calls to F are evaluated, and is 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 issues also an error on the following equivalent code that is accepted by the compiler:
This is enforced in SPARK by forbidding side-effects in functions, which
include updates to both parameters and global variables. As a consequence,
SPARK forbids functions with
in out parameters, as well as
functions updating a global variable. Thus function
F below is illegal in
SPARK, while function
Incr might be legal if it does not update any global
variables, and function
Incr_And_Log might be illegal if it updates global
variables for 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, these functions can easily be replaced by procedures with an
out parameter for returning the computed value.
When it has access to their body, GNATprove verifies which functions are indeed
free from side-effects. Here for example, the two functions
Incr_And_Log have the same signature, but only
Incr is legal in SPARK
Incr_And_Log is not as it attempts to update the global variable
No aliasing of names¶
Another restriction imposed in the SPARK subset concerns aliasing. We say that two names are aliased if they refer to the same object. There are two reasons to forbid aliasing in SPARK:
- First, it makes verification more difficult as it requires taking into account the fact that updates to two variables with different names may in fact update the same object.
- Then, results may seem unexpected from a user point of view. Indeed, when its parameters are aliased, the results of a subprogram call may depend on compiler specific treatment, like parameter passing mechanisms.
Since access types (pointers in Ada) are
not allowed in SPARK, aliasing can only occur as part of the parameter passing
in a subprogram call. As functions have no side-effects in SPARK, aliasing of
parameters in function calls is not problematic, so we only need to consider
procedure calls. When a procedure is called, SPARK makes sure that no
in out parameter is aliased with either another parameter
of the procedure or a global variable updated in the procedure's body.
Move_To_Total shows an example where the possibility of aliasing
was not taken into account by the programmer:
The example subprogram
Move_To_Total shown here increases the global
Total of the value of its input parameter
Source. It then
Source to 0. Here obviously, the programmer has not taken into
account the possibility of an aliasing between
is common practice. This subprogram is valid SPARK, and, for its verification,
GNATprove assumes, like the programmer, non-aliasing between
Source. To ensure that this assumption is correct, GNATprove will then
check for non-aliasing on every call to
Move_To_Total. The final call to
Move_To_Total in procedure
No_Aliasing violates this property, which
leads to both a message from GNATprove and a runtime error (assertion violation
corresponding to the expected increase in
Total from calling
Move_To_Total) when compiling and running. Note that the postcondition of
Move_To_Total is not violated on this second call, as integer parameters
are passes by copy, and the postcondition is checked here before the copy-back
from formal parameters to actual arguments.
Identifying SPARK Code¶
The SPARK language has been restricted to only allow easily specifiable and verifiable constructs. However, sometimes, a user cannot or does not want to abide by these limitations on all her code base. Therefore, the SPARK tools only check conformance to the SPARK subset on code which is identified as being in SPARK.
This can be done using an aspect named
SPARK_Mode. If not explicitly
SPARK_Mode is Off, which means that the code can use the
complete set of features from Ada and as a result should not be analyzed by
GNATprove. This default can be changed either selectively on some units or some
subprograms/packages inside units, or globally using a configuration pragma
like we're doing in this tutorial. To allow easy reuse of existing Ada
libraries, entities declared in imported units with no explicit
SPARK_Mode can still be used from SPARK code. The tool will only check
for SPARK conformance on the declaration of those entities which are
effectively used within the SPARK code.
Here is a common case of use of 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 ignored by GNATprove end P;
P only defines entities whose specifications are in the
SPARK subset. However, it can use all Ada features in its body which,
therefore, should not be analyzed and have the
set to Off.
SPARK_Mode can be specified in a fine-grained manner on a per-unit
basis. More precisely, a package has four different parts: the visible and
private parts of its specification, as well as the declarative and
statement part of its body. On each of these parts,
be specified to be either On or Off. In the same way, a subprogram has
two parts: its specification and its body.
A general rule in SPARK is that when
SPARK_Mode has been set to
Off, it can never be switched to On again. This prevents both setting
SPARK_Mode to On on subunits of a unit with
Off and switching back to
SPARK_Mode On on a part of a given
unit when a previous part had been set to Off.
Code Examples / Pitfalls¶
Here is a package defining an abstract stack type (defined as a private type in
Element objects along with some subprograms providing the usual
functionalities over stacks. It is marked to be 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 stack, where the unit
provides a single instance of stack. The content of the stack (global variables
Top) is not directly visible to clients. On this stripped
down version, only the function
Pop is available to clients. The unit spec
and body are marked to be in the SPARK subset.
Like previously, functions should be free from side-effects. Here,
updates 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, in the call to
Permute, actual values for parameters
are aliased, 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
On this example, we see the reason why aliasing is not allowed in
SPARK. Indeed, since
Positive, they are passed by
copy, and the result of the call to
Permute therefore depends on the order
in which they are 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, as two different
components of the same record object cannot refer to the same object.
Here is a slight modification of the previous example using an array
instead of a record.
Swap on values stored in
GNATprove detects a possible aliasing. Unlike the previous example, we have no
way here to know that the two elements
A (I) and
A (J) really are
distinct when we call
Swap. Note that GNATprove issues a check message here
instead of an error, so the user has the possibility to justify the message
We now consider a package declaring a type
Dictionary, which is an array
containing a word per letter. The procedure
Store allows to insert a word
at the correct index in a dictionary.
This code is not correct, as access types are not part of the SPARK
subset. In this case, they are really useful though, as, without them, we
cannot store arbitrarily long strings into an array. The solution here is
SPARK_Mode to separate parts of the access type from the
rest of the code in a fine grained manner.
Here is a modified version of the previous example. It has been adapted to hide
the access type inside the private part of package
SPARK_Mode (Off) at the start of the private part.
As 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
Although the body of
Store really uses no construct that are out of the
SPARK subset, it is not possible to set
body. Indeed, even if we don't use it, we have the visibility here on
private part which is not in SPARK.
Here, we have moved the declaration and the body of the procedure
another package named
Here everything is fine. We have managed to retain the use of the access type while having most of our code in the SPARK subset, so that GNATprove will be able to analyze it.
We now consider two functions searching for the value 0 inside an array
A. The first one raises an exception if 0 is not found in
A while the
other simply returns 0 in that case.
This code is perfectly correct, despite the use of exception handling. Indeed,
this non-SPARK feature is carefully isolated in a function body marked with a
Off, so that it is ignored by GNATprove. Remark that
GNATprove will try to demonstrate that
Not_Found will never be raised in
Search_Zero_P, leading to a message about a possible exception being
raised. Looking at
Search_Zero_N, it is indeed likely that an exception is
meant to be raised in some cases, which means that the user needs to verify
Not_Found is only raised when appropriate by other means like review