SPARK

From OpenProofsWiki

SPARK is a sub+superset of Ada, for developing highly safe or secure software. It was developed by Praxis High Integrity Systems.

As described in Wikipedia, "The 'SPARK Examiner' (part of the 'SPARK Toolset') performs two kinds of static analysis. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage can be incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (e.g., use of uninitialised data) on a system-wide basis (including abstract state in package bodies). The second, optional, analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds the Constraint_Error exception to the list of possible errors eliminated by SPARK. This proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties. It can also be used to show conformance with some suitable specification."

The specification can state that given certain preconditions, certain postconditions must hold. The "Examiner" then can generate a set of Verification Conditions (VCs). VCs are used to attempt to establish certain properties hold for a given subprogram. At a minimum, the Examiner will generate VCs attempting to establish that certain run-time errors cannot occur within a subprogram (e.g., array index out of range), as well as VCs for postconditions. The VCs can then be proved by either the SPADE Simplifier (an automated theorem prover) and the SPADE Proof Checker (a manual theorem prover, used for those VCs too difficult for the Simplifier).

The page What is Special About SPARK Contracts? gives a nice quick introduction to SPARK, which is excerpted here. It points out that the Ada line:

       procedure Inc (X : in out Integer);

just says there is some procedure “Inc” that may read a value X, and may write it out, but that’s it.

In SPARK, you can add much more precise information, and the SPARK tools can then check to see if they are true. For example, if you say this using SPARK:

       procedure Inc (X : in out Integer);
       --# global in out CallCount;
       --# pre  X < Integer'Last and
       --#      CallCount < Integer'Last;
       --# post X = X~ + 1 and 
       --#      CallCount = CallCount~ + 1;

With this more precise specification, the SPARK tools can ensure at compile-time (not run-time) that:

• X and global variable CallCount must be read by at least one path and must be updated by at least one path through the procedure
• Inc can only called when both X and CallCount are less than Integer’Last. The “pre” means “precondition”.
• After Inc runs, both X and CallCount will always be incremented by one (X~ refers to the initial value of X). The “post” means “postcondition”.

Tokeneer is an open proof built on SPARK.

The following provide more information about SPARK:

• Tokeneer Discovery is a tutorial on SPARK.
• The book "High Integrity Software: The SPARK Approach to Safety and Security" by John Barnes explains SPARK. Sampler text of Barnes' book is available online.
• SPARKAda.com provides a wide variety of information on SPARK.
• Wikipedia's article on the SPARK programming language