Category:SPARK: Difference between revisions

Content added Content deleted
m (Made Ada references into links)
(External -> wp link, added paradigms)
Line 9: Line 9:
|safety=safe
|safety=safe
|LCT=yes}}
|LCT=yes}}
{{language programming paradigm|concurrent}}
[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.
{{language programming paradigm|imparative}}
{{language programming paradigm|object-oriented}}
[[wp: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: