SPARK (programming Language)

SPARK (programming Language)

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.