SPARK programming language
Encyclopedia
SPARK is a formally-defined
computer
programming
language
based on the Ada
programming language, intended to be secure and to support the development of high integrity software
used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety (e.g., avionics in aircraft/spacecraft, or medical systems and process control software in nuclear powerplants) or for business integrity (for example financial software for banking and insurance companies).
There are two versions of the SPARK language; one based on Ada 83, and the other on Ada 95. The SPARK language consists of a highly restricted, well-defined subset of the Ada language that uses annotated meta information (in the form of Ada comments) that describe desired component behavior and individual runtime requirements, thereby optionally facilitating mandatory use of Design by Contract
principles to accurately formalize and validate expected runtime behavior.
Because the annotations are in commentary, SPARK programs are generally also valid Ada programs and can be compiled by an appropriate Ada compiler.
The most recent revision of the implementation, RavenSPARK, includes the Ravenscar tasking profile
which aims to support concurrency
in high integrity applications. The formal, unambiguous definition of SPARK allows and encourages a variety of static analysis
techniques to be applied to SPARK programs
.
.
These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking) and partly by introducing annotations or "formal comments" 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:
SPARK being an 'annotated subset' of Ada, programs written in SPARK can be compiled by any Ada compiler ('subset' of Ada implies that not all Ada features may be used).
'Annotated' means that certain annotations in form of Ada comments (i.e., ignored by the Ada compiler) are evaluated by an additional tool called the 'Examiner' which is meant to ensure strict enforcement of the requirements expressed via the aforementioned annotations to analyze the corresponding SPARK/Ada program for its correctness before passing it to an Ada compiler to compile the source code.
. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage can be incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (e.g., use of uninitialised data) on a system-wide basis (including abstract state in package bodies).
The second, optional, analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds the
to the list of possible errors eliminated by SPARK. This proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties. It can also be used to show conformance with some suitable specification.
procedure Increment (X : in out Counter_Type);
What does this subprogram actually do? In pure Ada, it could do virtually anything — it might increment the
With SPARK, annotations 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 (X : in out Counter_Type);
--# derives X from X;
or
procedure Increment (X : in out Counter_Type);
--# global Count;
--# derives
--# Count from Count, X &
--# X from ;
The first of these specifications tells us that the
If the Examiner 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 (precondition
s) or that will hold once execution of the subprogram has completed (postcondition
s). For example, we could say the following:
procedure Increment (X : in out Counter_Type);
--# derives X from X;
--# pre X < Counter_Type'Last;
--# post X = X~ + 1;
This specification now says that not only is
If a postcondition is added to the specification, the Examiner will also generate VCs that require the user to show that the postcondition will hold for all possible paths through the subprogram.
Discharging these proof obligations is performed using the SPADE Simplifier (an automated theorem prover) and the SPADE Proof Checker (a manual theorem prover, used for those VCs too thorny for the Simplifier to automatically discharge).
(with UK Ministry of Defence
sponsorship) 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 FLOSS
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 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 (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.
Formal semantics of programming languages
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
computer
Computer
A computer is a programmable machine designed to sequentially and automatically carry out a sequence of arithmetic or logical operations. The particular sequence of operations can be changed readily, allowing the computer to solve more than one kind of problem...
programming
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
based on the Ada
Ada (programming language)
Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
programming language, intended to be secure and to support the development of high integrity software
Computer software
Computer software, or just software, is a collection of computer programs and related data that provide the instructions for telling a computer what to do and how to do it....
used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety (e.g., avionics in aircraft/spacecraft, or medical systems and process control software in nuclear powerplants) or for business integrity (for example financial software for banking and insurance companies).
There are two versions of the SPARK language; one based on Ada 83, and the other on Ada 95. The SPARK language consists of a highly restricted, well-defined subset of the Ada language that uses annotated meta information (in the form of Ada comments) that describe desired component behavior and individual runtime requirements, thereby optionally facilitating mandatory use of Design by Contract
Design by contract
Design by contract , also known as programming by contract and design-by-contract programming, is an approach to designing computer software...
principles to accurately formalize and validate expected runtime behavior.
Because the annotations are in commentary, SPARK programs are generally also valid Ada programs and can be compiled by an appropriate Ada compiler.
The most recent revision of the implementation, RavenSPARK, includes the Ravenscar tasking profile
Ravenscar profile
The Ravenscar profile is a subset of the Ada tasking features designed for safety-critical hard real-time computing. It was defined by a separate technical report in Ada 95; it is now part of the Ada 2005 Standard.- Restrictions of the profile:...
which aims to support concurrency
Concurrency (computer science)
In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
in high integrity applications. The formal, unambiguous definition of SPARK allows and encourages a variety of static analysis
Static code analysis
Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
techniques to be applied to SPARK programs
Source code
In computer science, source code is text written using the format and syntax of the programming language that it is being written in. Such a language is specially designed to facilitate the work of computer programmers, who specify the actions to be performed by a computer mostly by writing source...
.
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 compilerCompiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
.
These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking) and partly by introducing annotations or "formal comments" 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:
- logical soundnessSoundnessIn mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
- rigorous formal definition
- simple semantics
- security
- expressive powerExpressive powerIn computer science, the expressive power of a language describes the ideas expressible in that language.For example, the Web Ontology Language expression language profile lacks ideas which can be expressed in OWL2 RL . OWL2 EL may therefore be said to have less expressive power than OWL2 RL...
- verifiability
- bounded resource (space and time) requirements.
- minimal runtime system requirements
SPARK being an 'annotated subset' of Ada, programs written in SPARK can be compiled by any Ada compiler ('subset' of Ada implies that not all Ada features may be used).
'Annotated' means that certain annotations in form of Ada comments (i.e., ignored by the Ada compiler) are evaluated by an additional tool called the 'Examiner' which is meant to ensure strict enforcement of the requirements expressed via the aforementioned annotations to analyze the corresponding SPARK/Ada program for its correctness before passing it to an Ada compiler to compile the source code.
Tool support
The "Examiner" (part of the "SPARK Toolset") performs two kinds of static analysisStatic code analysis
Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage can be incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (e.g., use of uninitialised data) on a system-wide basis (including abstract state in package bodies).
The second, optional, analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds the
Constraint_Error exceptionException handling
Exception handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
to the list of possible errors eliminated by SPARK. This proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties. It can also be used to show conformance with some suitable specification.
Annotation examples
Consider the Ada subprogram specification below:procedure Increment (X : in out Counter_Type);
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, annotations 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 (X : in out Counter_Type);
--# derives X from X;
or
procedure Increment (X : in out Counter_Type);
--# global Count;
--# derives
--# Count from Count, X &
--# X from ;
The first of these specifications tells us that the
Increment procedure does not update or read from any global variables and that the only data item used in calculating the new value of X is X itself. The second set of annotations tells us that Increment will use some global variable called "Count" in the same package as Increment and that the exported value of Count is dependent on the imported values of Count and X, but that exported value of X does not depend on any variables at all — it will be derived simply from constant data.If the Examiner 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
Information flow
In discourse-based grammatical theory, information flow is any tracking of referential information by speakers. Information may be new, just introduced into the conversation; given, already active in the speakers' consciousness; or old, no longer active...
. 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 (precondition
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....
s) or that will hold once execution of the subprogram has completed (postcondition
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 within the code itself...
s). For example, we could say the following:
procedure Increment (X : in out Counter_Type);
--# derives X from X;
--# pre X < Counter_Type'Last;
--# post X = X~ + 1;
This specification now says that not only is
X only derived from itself, but 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 — no more and no less.Verification Conditions
The Examiner can be requested to 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 Examiner will generate VCs attempting to establish that the following run-time errors cannot occur within a subprogram:- array index out of range
- type range violation
- division by zero
- numerical overflow.
If a postcondition is added to the specification, the Examiner will also generate VCs that require the user to show that the postcondition will hold for all possible paths through the subprogram.
Discharging these proof obligations is performed using the SPADE Simplifier (an automated theorem prover) and the SPADE Proof Checker (a manual theorem prover, used for those VCs too thorny for the Simplifier to automatically discharge).
History
The first version of SPARK (based on Ada 83) was produced at the University of SouthamptonUniversity of Southampton
The University of Southampton is a British public university located in the city of Southampton, England, a member of the Russell Group. The origins of the university can be dated back to the founding of the Hartley Institution in 1862 by Henry Robertson Hartley. In 1902, the Institution developed...
(with UK Ministry of Defence
Ministry of Defence (United Kingdom)
The Ministry of Defence is the United Kingdom government department responsible for implementation of government defence policy and is the headquarters of the British Armed Forces....
sponsorship) 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 FLOSS
Floss
Floss may refer to:* Dental floss, used to clean teeth* Embroidery thread, machine or hand-spun yarn for embroidery* Fairy floss or candyfloss, alternative names for cotton candy* Rousong, i.e. meat floss-Computing:...
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 August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein
Skein (hash function)
Skein is a cryptographic hash function and one out of five finalists in the NIST hash function competition to design what will become the SHA-3 standard, the intended successor of SHA-1 and SHA-2...
, 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 (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.
See also
- Z notationZ notationThe Z notation , named after Zermelo–Fraenkel set theory, 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:...
- Java Modeling LanguageJava Modeling LanguageThe Java Modeling Language is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...
- Extended static checkingExtended static checkingExtended Static Checking is a collective name for a range of techniques for statically checking the correctness of various program constraints. ESC can be thought of as an extended form of type checking. As with type checking, ESC is performed automatically at compile time...
- Static code analysisStatic code analysisStatic program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
- List of tools for static code analysis