SPARK (programming language)
 |
|
| Paradigm | Multi-paradigm |
|---|---|
| Developer | Altran and AdaCore |
| Stable release |
17.1 / March 14, 2017
|
| Typing discipline | static, strong, safe, nominative |
| OS | Cross-platform: Linux, Microsoft Windows, Mac OS X |
| License | GPLv3 |
| Website | SPARK Pro Toolset "Libre" SPARK GPL Edition |
| Major implementations | |
| SPARK Pro, SPARK GPL Edition | |
| Influenced by | |
| Ada, Eiffel | |
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 (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, 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 (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 "aspect" syntax 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 the entirety of the GNAT Ada 2012 front-end.
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 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:
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.
...
Wikipedia