Editing SPARK (programming language)

{{Short description|Programming language}}
{{About|the [[programming language]]|the [[cluster computing]] framework that can run on [[Scala (programming language)|Scala]], [[Java (programming language)|Java]], and [[Python (programming language)|Python]]|Apache Spark}}
{{Use dmy dates|date=April 2022}}
{{multiple issues|
{{More footnotes needed|date=September 2010}}
{{third-party|date=May 2014}}
}}
{{Infobox programming language
| name = SPARK
| logo = Sparkada.jpg
| logo size = 250px
| paradigm = [[Multi-paradigm programming language|Multi-paradigm]]: [[Structured programming|structured]], [[Imperative programming|imperative]], [[Object-oriented programming|object-oriented]], [[Aspect-oriented programming|aspect-oriented]],<ref>{{cite web|url=http://www.adacore.com/uploads/technical-papers/Ada2012_Rational_Introducion.pdf|title=Ada2012 Rationale|website=adacore.com|access-date=5 May 2018|url-status=live|archive-url=https://web.archive.org/web/20160418132340/http://www.adacore.com/uploads/technical-papers/Ada2012_Rational_Introducion.pdf|archive-date=18 April 2016}}</ref> [[Concurrent programming|concurrent]], [[Array programming|array]], [[Distributed computing|distributed]], [[Generic programming|generic]], [[Procedural programming|procedural]], [[Metaprogramming|meta]]
| family = [[Ada (programming language)|Ada]]
| developer = [[Altran]], [[AdaCore]]
| released = {{Start date and age|2009}}
| latest release version = Community 2021
| latest release date = {{Start date and age|2021|06|01}}
| typing = [[static typing|static]], [[Strong and weak typing|strong]], [[type safety|safe]], [[nominative type system|nominative]]
| operating system = [[Cross-platform]]: [[Linux]], [[Microsoft Windows|Windows]], [[macOS]]
| license = [[GNU General Public License|GPLv3]]
| website = {{URL|www.adacore.com/about-spark}}
| file ext =
| implementations = SPARK Pro, SPARK GPL Edition, SPARK Community
| dialects =
| influenced by = [[Ada (programming language)|Ada]], [[Eiffel (programming language)|Eiffel]]
| influenced =
}}

'''SPARK''' is a [[Formal semantics of programming languages|formally defined]] [[computer]] [[programming language]] based on the [[Ada (programming language)|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 [[software verification|verification]] tools.

The SPARK language consists of a well-defined subset of the Ada language that uses [[Design by contract|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 (programming languages)|syntax]] of ''[[Aspect-oriented programming|aspects]]'' to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the [[GNAT|GNAT/GCC]] infrastructure, and re-uses almost all of the GNAT Ada 2012 front-end.

== Technical overview ==
SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada [[compiler]]. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted [[task parallelism|parallel tasking]]) and partly by introducing contracts that encode the application designer's intentions and requirements for certain components of a program.

The combination of these approaches allows SPARK to meet its design objectives, which are:
* logical [[soundness]]
* rigorous formal definition
* simple semantics
* security
* [[expressive power (computer science)|expressive power]]
* [[Verification and validation|verifiability]]
* bounded resource (space and time) requirements.
* minimal runtime system requirements

== Contract examples ==
Consider the Ada subprogram specification below:

 '''procedure''' Increment (X : '''in out''' Counter_Type);

In pure Ada, this might increment the variable <code>X</code> by one or one thousand; or it might set some global counter to <code>X</code> and return the original value of the counter in <code>X</code>; or it might do nothing with <code>X</code>.

With SPARK 2014, contracts are added to the code to provide more information regarding what a subprogram actually does. For example, the above specification may be altered to say:

 '''procedure''' Increment (X : '''in out''' Counter_Type)
 '''  with''' Global => '''null''',
        Depends => (X => X);

This specifies that the <code>Increment</code> procedure uses no (neither update nor read) global variable and that the only data item used in calculating the new value of <code>X</code> is <code>X</code> alone.

Alternatively, may be specified:

 '''procedure''' Increment (X : '''in out''' Counter_Type)
 '''  with''' Global  => (In_Out => Count),
        Depends => (Count  => (Count, X),
                    X      => null);

This specifies that <code>Increment</code> will use the global variable <code>Count</code> in the same package as <code>Increment</code>, that the exported value of <code>Count</code> depends on the imported values of <code>Count</code> and <code>X</code>, and that the exported value of <code>X</code> does not depend on any variables at all and it will be derived from constant data only.

If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against what has been specified by the annotations and any discrepancies reported to the user.

These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (''[[precondition]]s'') or that will hold once execution of the subprogram has completed (''[[postcondition]]s''). For example, if writing:

 '''procedure''' Increment (X : '''in out''' Counter_Type)
 '''  with''' Global  => null,
        Depends => (X => X),
        Pre     => X < Counter_Type'Last,
        Post    => X = X'Old + 1;

This, now, specifies not only that <code>X</code> is derived from itself alone, but also that before <code>Increment</code> is called <code>X</code> must be strictly less than the last possible value of its type (to ensure that the result will never [[integer overflow|overflow]]) and that afterward <code>X</code> will be equal to the initial value of <code>X</code> plus one.

== Verification conditions ==
GNATprove can also generate a set of [[Verification condition generator|verification conditions]] (VCs). These are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as:
* array index out of range
* type range violation
* division by zero
* numerical overflow

If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram.

Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and the [[CVC4]], [[Z3 Theorem Prover|Z3]], and [[Alt-Ergo]] theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.

== History ==
The first version of SPARK (based on Ada 83) was produced at the [[University of Southampton]] (with UK [[Ministry of Defence (United Kingdom)|Ministry of Defence]] sponsorship) by Bernard Carré and Trevor Jennings. The name ''SPARK'' was derived from ''SPADE Ada Kernel'', in reference to the ''SPADE'' subset of the [[Pascal programming language]].<ref name=spark_lang_ref_manual>{{cite web |url=https://docs.adacore.com/sparkdocs-docs/SPARK_LRM.htm |title=SPARK – The SPADE Ada Kernel (including RavenSPARK) |publisher=AdaCore |access-date=2021-06-30}}</ref>

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

In early 2009, Praxis formed a partnership with AdaCore, and released ''SPARK Pro'' under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the [[free and open-source software]] (FOSS) and academic communities.

In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project ''[[Lunar IceCube|CubeSat]]'', expected to be completed in 2015.

In January 2013, Altran-Praxis changed its name to Altran, which in April 2021 became [[Capgemini Engineering]] (following Altran's merger with [[Capgemini]]).

The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the [[FLOSS]] and academic communities.

== Industrial applications ==

=== Safety-related systems ===
SPARK has been used in several high profile safety-critical systems, covering commercial aviation ([[Rolls-Royce Trent]] series jet engines, the [[ARINC ACAMS system]], the [[Lockheed Martin C-130J Super Hercules|Lockheed Martin C130J]]), military aviation ([[Eurofighter Typhoon|EuroFighter Typhoon]], [[Harrier GR9]], [[Aermacchi M-346|AerMacchi M346]]), air-traffic management (UK [[NATS iFACTS]] system), rail (numerous signalling applications), medical (the LifeFlow [[ventricular assist device]]), and space applications (the [[Vermont Lunar CubeSat|Vermont Technical College CubeSat project]]).{{citation needed|date=May 2022}}

=== Security-related systems ===
SPARK has also been used in secure systems development. Users include [[Rockwell Collins]] (Turnstile and SecureOne cross-domain solutions), the development of the original [[MULTOS]] CA, the NSA [[Tokeneer]] demonstrator, the secunet multi-level workstation, the Muen separation kernel and [[Genode]] block-device encrypter.

In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented [[Skein (hash function)|Skein]], one of candidates for [[Sha-3|SHA-3]], in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.<ref>{{cite news |url=http://www.sdtimes.com/link/34579 |title=Ada-derived Skein crypto shows SPARK |last=Handy |first=Alex |date=August 24, 2010 |work=[[SD Times]] |publisher=BZ Media LLC |accessdate=2010-08-31 }}</ref>

NVIDIA have also adopted SPARK for the implementation of security-critical firmware.<ref>{{cite web |url=https://www.slideshare.net/AdaCore/securing-the-future-of-safety-and-security-of-embedded-software |title = Securing the Future of Safety and Security of Embedded Software |date = 8 January 2020 }}</ref>

In 2020, Rod Chapman re-implemented the [[TweetNaCl]] cryptographic library in SPARK 2014.<ref>{{cite web |url=https://github.com/rod-chapman/SPARKNaCl |title = SPARKNaCl |website=[[GitHub]] |date = 8 October 2021 }}</ref> The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.

== See also ==
{{Portal|Free and open-source software}}
* [[Z notation]]
* [[Java Modeling Language]]

== References ==
{{Reflist}}

== Further reading ==

* {{cite book
 |last1=Barnes
 |first1= John
 |title=SPARK: The Proven Approach to High Integrity Software
 |date= 2012
 |publisher=Altran Praxis
 |ISBN=978-0-9572905-1-8
 |url=http://www.cpibookdelivery.com/book/9780957290518/SPARK__The_Proven_Approach_to_High_Integrity_Software
 |author-link=John Barnes (computer scientist)
}}

* {{cite book
 |last1=McCormick
 |first1=John W.
 <!-- author1 home page=https://www.cs.uni.edu/~mccormic/ -->
 |last2=Chapin
 |first2=Peter C.
 <!-- author2 home page=http://lemuria.cis.vermontstate.edu/~pchapin/ -->
 |title=Building High Integrity Applications with SPARK
 |date= 2015
 |publisher=Cambridge University Press
 |ISBN= 978-1-107-65684-0
 |url=http://www.cambridge.org/9781107656840
}}

* {{cite journal
 |last1=Ross
 |first1=Philip E.
 |date= September 2005
 |title=The Exterminators
 |journal=[[IEEE Spectrum]]
 |volume=42
 |issue=9
 |pages=36–41
 |issn= 0018-9235
 |url=https://spectrum.ieee.org/the-exterminators
 |doi=10.1109/MSPEC.2005.1502527
 |s2cid=26369398
|url-access=subscription
 }}

== External links ==
* [http://www.spark-2014.org/ SPARK 2014 community site]
* [http://www.adacore.com/sparkpro/ SPARK Pro website]
* [http://libre.adacore.com/ SPARK Libre (GPL) Edition website]
* [http://www.altran.com/ Altran]
* [http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf Correctness by Construction: A Manifesto for High-Integrity Software] {{Webarchive|url=https://web.archive.org/web/20121030153055/http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf |date=30 October 2012 }}
* [http://www.safety-club.org.uk/ UK's Safety-Critical Systems Club]
* [https://frama-c.com/html/fc-discuss/2009-November/msg00027.html Comparison with a C specification language (Frama C)]
* [http://www.adacore.com/tokeneer Tokeneer Project Page]
* [http://muen.codelabs.ch Muen Kernel Public Release]
* [http://lifeflow.mae.virginia.edu LifeFlow LVAD Project]
* [http://www.cubesatlab.org VTU CubeSat Project]

{{Authority control}}

{{DEFAULTSORT:Spark (Programming Language)}}
[[Category:Ada (programming language)]]
[[Category:Ada programming language family]]
[[Category:Algol programming language family]]
[[Category:Concurrent programming languages]]
[[Category:Formal specification languages]]
[[Category:High Integrity Programming Language]]
[[Category:History of computing in the United Kingdom]]
[[Category:Procedural programming languages]]
[[Category:Programming languages created in the 20th century]]
[[Category:Science and technology in Hampshire]]
[[Category:Statically typed programming languages]]
[[Category:Systems programming languages]]
[[Category:University of Southampton]]
<!-- Hidden categories below -->
[[Category:Articles with example Ada code]]