Anonymous user
Category:SPARK: Difference between revisions
m
Made Ada references into links
m (Further link correction) |
m (Made Ada references into links) |
||
Line 9:
|safety=safe
|LCT=yes}}
[http://en.wikipedia.org/wiki/SPARK_programming_language '''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:
Line 19:
*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.
| |||