SPARK (programming language)

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (September 2010) (Learn how and when to remove this message) This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. Please help improve it by replacing them with more appropriate citations to reliable, independent sources. (May 2014) (Learn how and when to remove this message) (Learn how and when to remove this message)

SPARK

Paradigm	Multi-paradigm: structured, imperative, object-oriented, aspect-oriented,[1] concurrent, array, distributed, generic, procedural, meta
Family	Ada
Developer	Altran, AdaCore
First appeared	2009; 16 years ago (2009)
Stable release	Community 2021 / June 1, 2021; 3 years ago (2021-06-01)
Typing discipline	static, strong, safe, nominative
OS	Cross-platform: Linux, Windows, macOS
License	GPLv3
Website	www.adacore.com/about-spark
Major implementations
SPARK Pro, SPARK GPL Edition, SPARK Community
Influenced by
Ada, Eiffel

SPARK is a formally defined computer programming language based on the Ada language, intended for developing high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates developing applications that demand safety, security, or business integrity.

Originally, three versions of SPARK existed (SPARK83, SPARK95, SPARK2005), based on Ada 83, Ada 95, and Ada 2005 respectively.

A fourth version, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supporting verification tools.

The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification.

In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK Examiner and its associated tools.

SPARK 2014, in contrast, uses Ada 2012's built-in syntax of aspects to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the GNAT/GCC infrastructure, and re-uses almost all of the GNAT Ada 2012 front-end.