Category:SPARK: Difference between revisions

← Older edit

Category:SPARK (view source)

Revision as of 12:22, 22 November 2016

1,040 bytes added , 7 years ago

add changed syntax coming with SPARK 2014

Oenone

256

edits

Revision as of 07:09, 12 August 2010 (view source) rosettacode>Dmitry-kazakov (Category created)		Latest revision as of 12:22, 22 November 2016 (view source) Oenone (talk \| contribs) (add changed syntax coming with SPARK 2014)
(15 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}} ~~'''SPARK''' or '''SPARK Ada''' is a programming language based on [[Ada]] used for high-integrity software development.~~ {{language programming paradigm\|imperative}} {{language programming paradigm\|object-oriented}} [[wp: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. The properties that SPARK code can be analysed for are: The key language feature are annotations used for static analysis of program semantics. A SPARK program without annotations is basically a legal [[Ada]] program. In relation to full [[Ada]], SPARK is a subset of, since the requirement of provability puts some constraints on which [[Ada]] constructs can be used. SPARK supports [[task\|multitasking]] and [[Ada]] concurrency mechanisms using a constraining tasking profile. Freedom from data-flow errors. Freedom from information flow errors. Freedom from information flows that violate safety or security. Type safety (freedom from run-time errors). Functional correctness. Absence of dead paths. In older versions, the annotations always 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. ~~The annotations are used by the Examiner in order to verify the program. For example, if the specified postconditions hold.~~ A SPARK program can be compiled by any [[Ada]] compiler or processed by any other [[Ada]] tool. The annotations state the required properties of a program. Different properties may require different types of annotation. 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 available from AdaCore at [http://docs.adacore.com/spark2014-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.