SPARK is a
formally defined computer
A computer is a machine that can be Computer programming, programmed to automatically Execution (computing), carry out sequences of arithmetic or logical operations (''computation''). Modern digital electronic computers can perform generic set ...
programming language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
based on the
Ada language, intended for developing
high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates developing applications that demand safety, security, or business integrity.
Originally, three versions of SPARK existed (SPARK83, SPARK95, SPARK2005), based on Ada 83, Ada 95, and Ada 2005 respectively.
A fourth version, 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
A contract is an agreement that specifies certain legally enforceable rights and obligations pertaining to two or more parties. A contract typically involves consent to transfer of goods, services, money, or promise to transfer any of thos ...
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 and so are ignored by any standard Ada compiler, but are processed by the SPARK ''Examiner'' and its associated tools.
SPARK 2014, in contrast, uses Ada 2012's built-in
syntax
In linguistics, syntax ( ) is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure (constituenc ...
of ''
aspects'' to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the
GNAT/GCC infrastructure, and re-uses almost all of the GNAT Ada 2012 front-end.
Technical overview
SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada
compiler
In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...
. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted
parallel tasking) and partly by introducing contracts that encode the application designer's intentions and requirements for certain components of a program.
The combination of these approaches allows SPARK to meet its design objectives, which are:
* logical
soundness
In logic and deductive reasoning, an argument is sound if it is both Validity (logic), valid in form and has no false premises. Soundness has a related meaning in mathematical logic, wherein a Formal system, formal system of logic is sound if and o ...
* rigorous formal definition
* simple semantics
* security
*
expressive power
*
verifiability
Verification or verify may refer to:
General
* Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
* bounded resource (space and time) requirements.
* minimal runtime system requirements
Contract examples
Consider the Ada subprogram specification below:
procedure Increment (X : in out Counter_Type);
In pure Ada, this might increment the variable
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 nothing with
X
.
With SPARK 2014, contracts are added to the code to provide more information regarding what a subprogram actually does. For example, the above specification may be altered to say:
procedure Increment (X : in out Counter_Type)
with Global => null,
Depends => (X => X);
This specifies that the
Increment
procedure uses no (neither update nor read) global variable and that the only data item used in calculating the new value of
X
is
X
alone.
Alternatively, may be specified:
procedure Increment (X : in out Counter_Type)
with Global => (In_Out => Count),
Depends => (Count => (Count, X),
X => null);
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 and it will be derived from constant data only.
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 what has been specified by the annotations and any discrepancies reported to the user.
These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (''
precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
If a precondition is violated, the effect of the ...
s'') or that will hold once execution of the subprogram has completed (''
postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions w ...
s''). For example, if writing:
procedure Increment (X : in out Counter_Type)
with Global => null,
Depends => (X => X),
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 (to ensure that the result will never
overflow) and that afterward
X
will be equal to the initial value of
X
plus one.
Verification conditions
GNATprove can also generate a set of
verification conditions (VCs). These are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as:
* array index out of range
* type range violation
* division by zero
* numerical overflow
If a postcondition or any other assertion is 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 (including interactive proof checkers) is also possible through other components of the Why3 toolset.
History
The first version of SPARK (based on Ada 83) was produced at the
University of Southampton
The University of Southampton (abbreviated as ''Soton'' in post-nominal letters) is a public university, public research university in Southampton, England. Southampton is a founding member of the Russell Group of research-intensive universit ...
(with UK
Ministry of Defence sponsorship) by Bernard Carré and Trevor Jennings. The name ''SPARK'' was derived from ''SPADE Ada Kernel'', in reference to the ''SPADE'' subset of the
Pascal programming language.
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
free and open-source software
Free and open-source software (FOSS) is software available under a license that grants users the right to use, modify, and distribute the software modified or not to everyone free of charge. FOSS is an inclusive umbrella term encompassing free ...
(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
A CubeSat is a class of small satellite with a form factor of cubes. CubeSats have a mass of no more than per unit,, url=https://static1.squarespace.com/static/5418c831e4b0fa4ecac1bacd/t/5f24997b6deea10cc52bb016/1596234122437/CDS+REV14+2020-07-3 ...
'', expected to be completed in 2015.
In January 2013, Altran-Praxis changed its name to Altran, which in April 2021 became
Capgemini Engineering
Capgemini Engineering (previously known as ''Altran Technologies, SA'') is a global innovation and engineering consulting firm founded in 1982 in France by Alexis Kniazeff and Hubert Martigny.
Altran Technologies operated primarily in high tec ...
(following Altran's merger with
Capgemini
Capgemini SE is a French Multinational corporation, multinational information technology (IT) services and consulting company, headquartered in Paris, France.
History
Capgemini was founded by Serge Kampf in 1967 as an enterprise management and d ...
).
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 (
Rolls-Royce Trent
The Rolls-Royce Trent is a family of high-bypass turbofans produced by Rolls-Royce Holdings, Rolls-Royce. It continues the Turbofan#Three-spool, three spool architecture of the Rolls-Royce RB211, RB211 with a maximum thrust ranging from . Lau ...
series jet engines, the
ARINC ACAMS system, the
Lockheed Martin C130J), military aviation (
EuroFighter Typhoon,
Harrier GR9,
AerMacchi M346), air-traffic management (UK
NATS iFACTS system), rail (numerous signalling applications), medical (the LifeFlow
ventricular assist device), and space applications (the
Vermont Technical College CubeSat project).
Security-related systems
SPARK has also been used in secure systems development. Users include
Rockwell Collins
Rockwell Collins, Inc. was a multinational corporation headquartered in Cedar Rapids, Iowa, providing avionics and information technology systems and services to government agencies and aircraft manufacturers. It was formed when the Collins Radi ...
(Turnstile and SecureOne cross-domain solutions), 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. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.
NVIDIA have also adopted SPARK for the implementation of security-critical firmware.
In 2020, Rod Chapman re-implemented the
TweetNaCl cryptographic library in SPARK 2014.
The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.
See also
*
Z notation
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
History
In 1974, Jean-Raymond Abria ...
*
Java Modeling Language
References
Further reading
*
*
*
External links
SPARK 2014 community siteSPARK Pro websiteSPARK Libre (GPL) Edition websiteAltranCorrectness by Construction: A Manifesto for High-Integrity Software
UK's Safety-Critical Systems ClubTokeneer Project PageMuen Kernel Public ReleaseLifeFlow LVAD ProjectVTU CubeSat Project
{{DEFAULTSORT:Spark (Programming Language)
Ada (programming language)
Ada programming language family
Algol programming language family
Concurrent programming languages
Formal specification languages
High-integrity programming languages
History of computing in the United Kingdom
Procedural programming languages
Programming languages created in the 20th century
Science and technology in Hampshire
Statically typed programming languages
Systems programming languages
University of Southampton
Articles with example Ada code