SPARK Hi-Lite GPL Edition
2013 GPL Edition Now Available!
SPARK Hi-Lite GPL 2013 is a package that can be installed after GNAT GPL 2013, to provide access to the new SPARK toolset developed in project Hi-Lite . This release is a major evolution of the SPARK toolset providing formal verification for a subset of Ada programs. This new toolset uses Ada 2012-style contracts (e.g. pre- and postconditions), instead of the stylized comments in previous versions, to provide specifications of programs. The benefits of this new version are:
- - larger supported subset of Ada (including generics, discriminants, etc.)
- - same contracts used for testing and formal verification
- - applicable to units partly in SPARK
- - improved automatic proof of complex contracts
- - new integration in GPS
AdaCore and Altran are dedicated to developing the finest tools available for software development with SPARK and Ada. The SPARK GPL Edition is the development environment for Free Software development and the GNAT Academic Program for use in Academia. SPARK Pro is for commercial/industrial development.
- Automatic selection of flow analysis mode – the Examiner now supports automatic selection of information flow or data flow analysis on a per subprogram basis.
- Derived Numeric Types – definition of numeric types has been made easier in GPL 2012 by the introduction of language and tool support for explicitly derived numeric types.
- SPARKBridge preview for Windows – SPARKBridge, a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers – is now available as a preview to Windows users, allowing them to trial alternate provers for discharging Verification Conditions.
- Library Additions – the SPARK library has been augmented with several new packages including: Interfaces, Ada.Characters.Handling, Ada.Text_IO
Improvements to Proof Tools - the Simplifier now has enhanced reasoning capabilities for modular types, allowing more proofs to be automatically discharged. In addition, the proof summary output (from the POGS tool) has been improved to make the management of the proof process easier for large projects.
- The SPARK Language Definition
- Full SPARK Toolset, including Examiner, Simplifier and Checker
- Supporting SPARK tools: SPARKSimp, SPARKMake, SPARKFormat and POGS, ViCToR Wrapper, and ZombieScope
- Tutorial material for SPARK GPL and SPARK Pro are included in the accompanying release of the Tokeneer Discovery package.