Category:SPARK: Difference between revisions
m (Corrected link.) |
m (Further link correction) |
||
| Line 25: | Line 25: | ||
The annotations state the required properties of a program. Different properties may require different types of annotation. |
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 [[ |
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 - the main copyright is held by [http://www.sparkada.com/ Altran-Praxis]. |
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 17:12, 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.