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.
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.