Category:SPARK
This programming language may be used to instruct a computer to perform a task.
Official website |
---|
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 |
Lang tag(s): | spark |
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.
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.
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 available from AdaCore at SPARK 2014 Reference Manual.
The comp.lang.ada newsgroup (access via Google Groups)is the main forum for discussing or asking questions about SPARK.
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.