SPARK Ada
SPARK is a formally-defined computer programming language based on Ada, 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 or security, or to satisfy other business-critical requirements for trustworthy software.
SPARK aims to exploit the strengths of Ada by producing programs that are unambiguous and have behavior that is independent of the choice of compiler. These goals are achieved partly by using a well-defined subset of the Ada language and partly by introducing contracts which encode the application designer’s intentions and requirements for certain components of a program.
The formal, unambiguous, definition of SPARK allows and encourages a variety of static analysis techniques to be applied to SPARK programs. These include information flow analysis, proof of absence of run-time exceptions, proof of functional correctness, and proof of safety and security properties. Proof of termination is now also possible using loop variant contracts.
There have been four versions of the SPARK language based on Ada 83, Ada 95, Ada 2005 and Ada 2012 respectively. The most recent version, SPARK 2014, is based on Ada 2012 and represents a complete re-design of the language and supporting verification tools. You can find out more about SPARK 2014 – including a full language reference manual – on the dedicated website http://www.spark-2014.org/about. The website also includes a blog that will keep you up to date with on-going projects and further developments with the SPARK language (see http://www.spark-2014.org).
