SPARK Discovery

SPARK Discovery brings the advantages of formal methods to GNAT Pro users. With SPARK Discovery you can verify that variables are initialized before use, that data and information flows are correct, and that the code is free from run-time errors.

The SPARK subset of Ada is amenable to formal analysis, bringing mathematics based assurance to the verification of program properties ranging from data architecture consistency (proper uses of variables and subprogram parameters) to functional correctness. SPARK Discovery, included in each GNAT Pro product, is a basic toolset that lets you take advantage of formal methods in an incremental manner that fits in with your project's workflow. And since SPARK uses Ada's contract-based programming features, you can write contracts that are checked dynamically (Ada semantics) or statically (SPARK proof), and "mix and match" code that is verified by testing and by formal methods.

Formal methods can be applied at various levels of software assurance. SPARK Discovery is appropriate at the Stone level (adherence to the SPARK subset), the Bronze level (Stone plus verification of data flow / check for references to uninitialized variables), and the Silver level (Bronze + absence of run-time errors).  The full SPARK Pro product is more appropriate at the higher levels: Gold (Silver + proof of integrity properties) and Platinum (Gold + proof of functional correctness). Please refer to the SPARK User's Guide for a complete description of the differences between SPARK Discovery and SPARK Pro.

Implementation Guidance for the Adoption of SPARK

If you are interested in taking advantage of the benefits of SPARK, please look at the guidance document that we have written with Thales (France) which details the steps that should be taken to adopt SPARK, along with the costs and benefits of doing so. The document describes the five levels of software assurance that can be achieved with SPARK: Stone, Bronze, Silver, Gold and Platinum. The document is available online:

www.adacore.com/knowledge/tech...

or contact us at info@adacore.com to receive a paper copy.