SPARK
SPARK
This programming language may be used to instruct a computer to perform a task.
Listed below are all of the tasks on Rosetta Code which have been solved using 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.