SPARK (programming language)
|This article needs additional citations for verification. (September 2010)|
|Designed by||Bernard Carré and Trevor Jennings|
|Stable release||10.1.0 (January 4, 2012)|
|Typing discipline||static, strong, safe, nominative|
|Major implementations||SPARK Pro, SPARK GPL Edition|
|Influenced by||Ada, HAL/S|
|OS||Cross-platform: Linux, Microsoft Windows, Solaris, Mac OS X|
|Website||SPARK Pro Toolset "Libre" SPARK GPL Edition|
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 three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively. A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, is currently in development and expected to be released Q1 2014. 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 SPARK83/95/2005 annotations are encoded in Ada comments, SPARK programs are generally also valid Ada programs and can be compiled by an appropriate Ada compiler. In the future, SPARK 2014 will use the Ada 2012 language feature called aspects to replace the comment based annotations.
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.
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 (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 soundness
- rigorous formal definition
- simple semantics
- expressive power
- 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.
The "Examiner" (part of the "SPARK Toolset") performs two kinds of static analysis. 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 exception 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.
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;
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
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. 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 (preconditions) or that will hold once execution of the subprogram has completed (postconditions). 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.
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).
The first version of SPARK (based on Ada 83) was produced at the University of Southampton (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.
In January 2013 Altran-Praxis changed its name to Altran.
- Z notation
- Java Modeling Language
- Extended static checking
- Static code analysis
- List of tools for static code analysis
||This article includes a list of references, but its sources remain unclear because it has insufficient inline citations. (September 2010)|
- John Barnes (June 15, 1997). High Integrity Ada: The SPARK Approach. Addison-Wesley. ISBN 0-201-17517-7.
- John Barnes (April 25, 2003). High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley. ISBN 0-321-13616-0.
- Philip E. Ross (September 2005). "The Exterminators". IEEE Spectrum 42 (9): 36–41. doi:10.1109/MSPEC.2005.1502527. ISSN 0018-9235.