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.

Read more about SPARK (programming Language):  Technical Overview, Tool Support, Annotation Examples, Verification Conditions, History

Other articles related to "spark":

SPARK (programming Language) - History
... 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 ... 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 ...

Famous quotes containing the word spark:

    In general, one may pronounce kissing dangerous. A spark of fire has often been struck out of the collision of lips, that has blown up the whole magazine of virtue.
    Anonymous, U.S. women’s magazine contributor. Weekly Visitor or Ladies Miscellany, p. 203 (April 1803)