Spark Pro – Language & Toolsuite
High Assurance Software Development
SPARK Pro combines the power of the SPARK language and toolsuite from Praxis with the GPS development environment from AdaCore in a single package.
SPARK Language
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.
SPARK Examiner
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.
Learn more
SPARK Simplifier
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.
Blackbelt Edition
SPARK Pro BlackBelt Edition adds support for two optional components of the toolsuite: the Proof Checker and the RavenSPARK language option.
SPARK Proof Checker
The Proof Checker is an interactive proof tool that uses the same logic and inference engine as the Simplifier. It can be used to complete the proof of any VCs left undischarged by the Simplifier, if the assurance requirements of the project are high enough to warrant a fully formal proof.
RavenSPARK Language Option
The RavenSPARK option brings the power of Ada’s Ravenscar tasking profile to SPARK, enabling engineers to design concurrent software without sacrificing verification or assurance. RavenSPARK is specifically design to be compatible with hard real-time operating systems, all implementations of the Ravenscar profile, and to be amenable to the static analysis of worst-case execution time, schedulability and memory consumption.
More on SPARK Pro
Frontline Support »
Learn about the other side of SPARK Pro
The world’s largest team of SPARK experts at your fingertips
Continue Reading
SPARK Pro Overview »
SPARK Pro is a language, toolsuite and design approach
for the development of high assurance software. SPARK has
an enviable track-record in many industry sectors, such as
aerospace, rail, nuclear and security, and has been used
to meet or exceed all known industry guidance and standards
at the highest assurance levels.
Continue Reading
The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC(tm) architecture.