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 programming language based on Ada used for high-integrity software development.
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 multitasking and Ada concurrency mechanisms using a constraining tasking profile.
The annotations are used by the Examiner in order to verify the program. For example, if the specified postconditions hold.
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.