Category:SPARK
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.
- Execution method/Compiled/Machine code
- Garbage collection/Allowed
- Parameter passing/By reference
- Parameter passing/By value
- Typing/Safe
- Typing/Strong
- Typing/Compatibility/Nominative
- Typing/Expression/Explicit
- Typing/Checking/Static
- Programming Languages
- Programming paradigm/Concurrent
- Programming paradigm/Imparative
- Programming paradigm/Object-oriented