SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential.
SPARK Pro 11 offers many enhancements particularly in the area of program proof. For example a number of significant enhancements have been made to the way that functions and proof functions are handled in SPARK Pro 11. These changes will improve project efficiency by eliminating the vast majority of rules that were previously manually encoded.
The main changes include a more powerful language for specifying proof functions and the ability to use the functions in any proof context. This greatly simplifies the task of writing and maintaining functional contracts for critical software, providing high-assurance at lower cost.
It also includes counter-example generation and makes the proof function an even more powerful technique for achieving high levels of assurance in safety or security-critical software.
In the past, when performing proofs users typically spent much of their time inspecting undischarged “verification conditions” to determine whether they can indeed be proved.
Included with SPARK Pro 11, Riposte is a new tool that not only determines whether a verification condition is false, but can also generate a counter-example to demonstrate the conditions under which it is false.
Jointly developed by Altran Praxis and the University of Bath (UK), Riposte is a major improvement to the verification workflow, saving projects a significant amount of time previously spent analyzing unprovable verification conditions and providing developers with intuitive explanations.
A new assume contract in SPARK Pro 11 allows users to introduce system-level assumptions about programs into their proofs in a clear and concise format. Previously, these assumptions might have been captured by user rules or manual review.
SPARK Pro combines Altran Praxis' SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments from AdaCore. There are SPARK versions based on Ada 83, Ada 95, and Ada 2005, so all standard Ada compilers and tools work out-of-the-box with SPARK.
SPARK Pro is specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency.
The toolset generates evidence for correctness, including proofs of the absence of run-time errors, that can be used to meet the requirements of safety and security certification schemes such as DO-178B, DO-178C, and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.
SPARK Pro 11 is available now. A demonstration providing an introduction to the new features in SPARK Pro 11 is available now at http://adaco.re/2h.