Category:SPARK: Difference between revisions
Content added Content deleted
m (Further link correction) |
m (Made Ada references into links) |
||
| Line 9: | Line 9: | ||
|safety=safe |
|safety=safe |
||
|LCT=yes}} |
|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. |
[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: |
The properties that SPARK code can be analysed for are: |
||
| Line 19: | Line 19: | ||
*Absence of dead paths. |
*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. |
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. |
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. |
The annotations state the required properties of a program. Different properties may require different types of annotation. |
||