Category:SPARK: Difference between revisions
(Category created) |
(Amended SPARK language description.) |
||
| Line 9: | Line 9: | ||
|safety=safe |
|safety=safe |
||
|LCT=yes}} |
|LCT=yes}} |
||
'''SPARK''' or '''SPARK Ada''' is a |
[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. |
||
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 |
The annotations always begin, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the Ada standard. |
||
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]. |
|||
Revision as of 16:08, 19 August 2010
This programming language may be used to instruct a computer to perform a task.
| Execution method: | Compiled (machine code) |
|---|---|
| Garbage collected: | Allowed |
| Parameter passing methods: | By reference, By value |
| Type safety: | Safe |
| Type strength: | Strong |
| Type compatibility: | Nominative |
| Type expression: | Explicit |
| Type checking: | Static |
| See Also: |
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:
- 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 always begin, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the Ada standard.
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 here.
The SPARK tools are freely available under the GNU GPL. The SPARK language definition is proprietary - the main copyright is held by Altran-Praxis.
Subcategories
This category has the following 3 subcategories, out of 3 total.
@
- SPARK examples needing attention (empty)
- SPARK Implementations (1 P)
- SPARK User (3 P)
Pages in category "SPARK"
The following 8 pages are in this category, out of 8 total.