SPARK
'''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: *Freedom from data-flow errors. *Freedom from information flow errors. *Freedom from information flows that violate safety or security. *Type safety (freedom from run-time errors). *Functional correctness. *Absence of dead paths.
In older versions, the annotations always began, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the Ada standard. Newer versions, starting with SPARK 2014, use the aspect syntax known from Ada 2012.
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.
A description of the SPARK Proof process is here.
The SPARK tools are freely available under the GNU GPL. The SPARK language definition is available from AdaCore at SPARK 2014 Reference Manual.
The [news:comp.lang.ada comp.lang.ada] newsgroup (access via Google Groups)is the main forum for discussing or asking questions about SPARK.