SPARK: Difference between revisions
Content added Content deleted
(New language) |
(Redirect to Category:SPARK) |
||
| Line 1: | Line 1: | ||
#REDIRECT [[:Category:SPARK]] |
|||
{{language|SPARK |
|||
|exec=machine |
|||
|gc=allowed |
|||
|parampass=both |
|||
|checking=static |
|||
|compat=nominative |
|||
|express=explicit |
|||
|strength=strong |
|||
|safety=safe |
|||
|LCT=yes}} |
|||
'''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 [[task|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. |
|||
Latest revision as of 07:10, 12 August 2010
Redirect to: