SPARK and Compilers

SPARK is designed to eliminate all instances of erroneous behaviour in programs. SPARK programs can also be shown to be free from bounded errors and implementation dependencies, so SPARK programs have the same dynamic semantics, regardless of compiler and target – in short, SPARK is a remarkably portable language.

Secondly, SPARK has been expressly designed to require no supporting runtime library, which makes it ideal for systems where certification of such libraries remains an expensive or difficult proposition.

SPARK is fully compatible with all the various high-integrity runtime options from all the major Ada compiler vendors, including:

SCORE and SCORE-653 for CsLEOS from DDC-I.

GNAT Pro High-Integrity Edition from AdaCore. For more information about with use of SPARK with GNAT Pro, see the Publications page.

AdaMagic from SofCheck.

SMART, C-SMART and ObjectAdaTM/RavenTM from Aonix.

VADSsc and APEX®/MARK from Rational.

GMART from Green Hills Software.

ERC32 and 1750A Ada from XGC Software.