Category:SPARK

SPARK
This programming language may be used to instruct a computer to perform a task.

Official website

Execution method:	Compiled (machine code)
Garbage collected:	Allowed
Parameter passing methods:	By reference, By value
Type safety:	Safe
Type strength:	Strong
Type compatibility:	Nominative
Type expression:	Explicit
Type checking:	Static
Lang tag(s):	spark
See Also:	SPARK on the HOPL SPARK compared to other languages

Listed below are all of the tasks on Rosetta Code which have been solved using 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 comp.lang.ada newsgroup (access via Google Groups)is the main forum for discussing or asking questions about SPARK.