Category:SPARK

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

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):	Ada
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.

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.

A description of the SPARK Proof process is here.

The SPARK tools are freely available under the GNU GPL. The SPARK language definition is proprietary - the main copyright is held by Altran-Praxis.