Category:SPARK: Difference between revisions
add changed syntax coming with SPARK 2014
m (Made Ada references into links) |
(add changed syntax coming with SPARK 2014) |
||
| (11 intermediate revisions by 6 users not shown) | |||
Line 1:
{{language|SPARK
|site=http://www.altran-praxis.com/spark.aspx
|tags=spark
|exec=machine
|gc=allowed
Line 9 ⟶ 11:
|safety=safe
|LCT=yes}}
{{language programming paradigm|concurrent}}
[http://en.wikipedia.org/wiki/SPARK_programming_language '''SPARK'''] or '''SPARK Ada''' is a sub-language of [[Ada]], supplemented with annotations (formal comments). Its primary purpose is for high-integrity applications, where static analysis of the source is used to determine properties of the program.▼
{{language programming paradigm|imperative}}
{{language programming paradigm|object-oriented}}
▲[
The properties that SPARK code can be analysed for are:
Line 19 ⟶ 24:
*Absence of dead paths.
A SPARK program can be compiled by any [[Ada]] compiler or processed by any other [[Ada]] tool.
Line 27 ⟶ 32:
A description of the SPARK Proof process is [[SPARK_Proof_Process|here]].
The SPARK tools are freely available under the GNU GPL. The SPARK language definition is
The [news:comp.lang.ada comp.lang.ada] [[newsgroup]] ([http://groups.google.com/group/comp.lang.ada/topics access via Google Groups])is the main forum for discussing or asking questions about SPARK.
| |||