Rosetta Code

Category:SPARK: Difference between revisions

Category Discussion

Category:SPARK (view source)

Revision as of 16:08, 19 August 2010

540 bytes added ,  13 years ago
Amended SPARK language description.
(Category created)
 
(Amended SPARK language description.)
Line 9:
|safety=safe
|LCT=yes}}
[http://en.wikipedia.org/wiki/SPARK_programming_language '''SPARK'''] or '''SPARK Ada''' is a programming sub-language basedof on [[Ada]], usedsupplemented with annotations (formal comments). Its primary purpose is for high-integrity softwareapplications, where static analysis of the source is used to determine properties of the developmentprogram.
 
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.
 
The annotations arealways usedbegin, on each line, bywith the ExaminerAda incomment ordersymbol to“--”, verifyso theall program.SPARK Forprograms example,comply ifwith the specifiedAda postconditions holdstandard.
 
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 [[Encyclopedia:SPARK Proof Process|here]].
 
The SPARK tools are freely available under the GNU GPL. The SPARK language definition is proprietary - the main copyright is held by [http://www.sparkada.com/ Altran-Praxis].
Retrieved from "https://rosettacode.org/wiki/Special:MobileDiff/154869"