SPARK (programming language)


SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity.
Originally, there were three versions of the SPARK language based on Ada 83, Ada 95 and Ada 2005 respectively.
A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supporting verification tools.
The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification.
In SPARK83/95/2005, the contracts are encoded in Ada comments, but are processed by the SPARK "Examiner" and its associated tools.
SPARK 2014, in contrast, uses Ada 2012's built-in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 is based on the GNAT/GCC infrastructure, and re-uses almost the entirety of the GNAT Ada 2012 front-end.

Technical overview

SPARK aims to exploit the strengths of Ada while trying to eliminate all its potential ambiguities and insecurities. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada compiler. These goals are achieved partly by omitting some of Ada's more problematic features and partly by introducing contracts which encode the application designer's intentions and requirements for certain components of a program.
The combination of these approaches is meant to allow SPARK to meet its design objectives, which are:
Consider the Ada subprogram specification below:
procedure Increment ;
What does this subprogram actually do? In pure Ada, it could do virtually anything – it might increment the X by one or one thousand; or it might set some global counter to X and return the original value of the counter in X; or it might do absolutely nothing with X at all.
With SPARK 2014, contracts are added to the code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say:
procedure Increment
with Global => null,
Depends => ;
This specifies that the Increment procedure does not use any global variable and that the only data item used in calculating the new value of X is X itself.
Alternatively, the designer might specify:
procedure Increment
with Global =>,
Depends => ;
This specifies that Increment will use the global variable Count in the same package as Increment, that the exported value of Count depends on the imported values of Count and X, and that the exported value of X does not depend on any variables at all.
If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against that which has been specified by the annotations and any discrepancies reported to the user.
We can further extend these specifications by asserting various properties that either need to hold when a subprogram is called or that will hold once execution of the subprogram has completed. For example, we could say the following:
procedure Increment
with Global => null,
Depends =>,
Pre => X < Counter_Type'Last,
Post => X = X'Old + 1;
This, now, specifies not only that X is derived from itself alone, but also that before Increment is called X must be strictly less than the last possible value of its type and that afterwards X will be equal to the initial value of X plus one.

Verification conditions

GNATprove can also generate a set of verification conditions or VCs. VCs are used to attempt to establish certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs attempting to establish that all run-time errors cannot occur within a subprogram, such as
If a postcondition or other assertions are added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram.
Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and the CVC4, Z3, and Alt-Ergo theorem provers to discharge VCs. Use of other provers is also possible through other components of the Why3 toolset.

History

The first version of SPARK was produced at the University of Southampton by Bernard Carré and Trevor Jennings. Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company became Altran Praxis.
In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the FOSS and academic communities.
In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project CubeSat, expected to be completed in 2015.
In January 2013, Altran-Praxis changed its name to Altran.
The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the FLOSS and academic communities.

Industrial applications

Safety-related systems

SPARK has been used in several high profile safety-critical systems, covering commercial aviation, military aviation, air-traffic management, rail, medical, and space applications.

Security-related systems

SPARK has also been used in secure systems development. Users include Rockwell Collins, the development of the original MULTOS CA, the NSA Tokeneer demonstrator, the secunet multi-level workstation, the Muen separation kernel and Genode block-device encrypter.
In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein, one of candidates for SHA-3, in SPARK. He wanted to compare the performance of the SPARK and C implementations. After careful optimization, he managed to have the SPARK version only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC closed the gap, with the SPARK code matching the C in performance exactly.