SPARK (programming language)

SPARK is a formally defined programming language based on a well-defined subset of Ada, intended for building high-integrity software where predictable and reliable behavior is essential. It removes Ada constructs that can behave unpredictably and adds contracts that describe what each component does, so that both static and dynamic verification are possible. Early versions based on Ada 83, 95 and 2005 kept contracts in comments and relied on the SPARK Examiner, while SPARK 2014, released on April 30, 2014 and based on Ada 2012, was a redesign that uses Ada aspects and the GNATprove tool. The language began in 1987 at the University of Southampton and was later developed by Praxis and then Altran and AdaCore. It is used in avionics, rail signalling, medical devices and security systems.