SPARK Pro is an open source development environment created by Praxis and AdaCore. SPARK Pro combines the SPARK language and toolset with the AdaCore GNAT Programming Studio (GPS) Integrated Development Environment (IDE). SPARK, which was developed by Praxis, is a language designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. The new development environment is available now from AdaCore. Existing SPARK users have the option to transition to the new environment, which is also available as a standalone product.
The SPARK Language takes a radical step away from contemporary programming language design. The primary design goal is the provision of a sound verification framework and toolsuite which renders many common defects simply impossible or at least sure to be detected. The SPARK language embodies a stictly defined and enforced subset of Ada complemented by an expressive system of contracts that precisely convey the design or the specification of the program itself.
The SPARK Examiner provides the main static analysis engine of SPARK Pro. It enforces the SPARK subset and static semantics, checks contracts for consistency with source code, and implements the SPARK information-flow analysis and verification condition generator.
GNAT Programming Studio – IDE
This Integrated Development Environment serves as your portal to the GNAT Pro toolchain. It provides customizable settings, browsing, syntax-directed editing, easy integration with third party tools such as Version Control Systems, source navigation, dependency graphs, and more.
The Simplifier is an automated theorem prover that processes the verification conditions (VCs) produced by the Examiner. The proof of these VCs confirms critical program properties, such as the freedom from run-time errors and exceptions, or specific safety and security properties. For well-written code, the Simplifier typically proves over 95% of these VCs completely automatically – or, in other words, less than a 5% false-alarm rate.
SPARK Supporting Tools
SPARK pro also includes other supporting tools for SPARK such as a pretty-printer for contracts (SPARKFormat), a proof status summarizer (POGS), and the SPARKMake tool for generating the Examiner’s index- and meta-files.
GNAT Semantic Analyzer
The GNAT Semantic Analyzer provides a full Ada front-end capability in support of SPARK Pro. This offers full Ada static semantic checking, style checking, and generation of cross-reference information for use within the GPS IDE.