Category:SPARK: Difference between revisions

Category:SPARK (view source)

276 bytes added , 7 years ago

add changed syntax coming with SPARK 2014

256

edits

Revision as of 08:23, 20 August 2010 (view source) rosettacode>PhilThornley m (Added reference to c.l.a for talking about SPARK.) ← Older edit		Latest revision as of 12:22, 22 November 2016 (view source) Oenone (talk \| contribs) (add changed syntax coming with SPARK 2014)
(5 intermediate revisions by 5 users not shown)
Line 1: {{language\|SPARK \|site=http://www.altran-praxis.com/spark.aspx \|tags=~~Ada~~spark \|exec=machine \|gc=allowed Line 23 ⟶ 24: *Absence of dead paths. ~~The~~In older versions, the annotations always ~~begin~~began, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the [[Ada]] standard. Newer versions, starting with SPARK 2014, use the aspect syntax known from Ada 2012. A SPARK program can be compiled by any [[Ada]] compiler or processed by any other [[Ada]] tool. Line 31 ⟶ 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 ~~proprietary~~available -from ~~the~~AdaCore ~~main copyright is held by~~at [http://~~www~~docs.~~sparkada~~adacore.com/ ~~Altran~~spark2014-~~Praxis~~docs/html/lrm/ SPARK 2014 Reference Manual]. 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.