SPARK Pro 10.1
AdaCore is pleased to announce the availability of SPARK Pro 10.1 on the following platforms:
This is a major release including many new features:
- Generics Phase 1 - Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
- Dynamic Flow Analyser and VCG Heaps
- Unicode characters now allowed in strings
- Improved use of types and subtypes in FDL
- Improvements to Simplifier tactics and performance
- Auto-generation of refinement rules
- Improvements to SPARKBridge
- New SPARKClean utility
The new features will be presented in a webinar on Tuesday February 21st, 2012.
For more information and to register, please visit:
Further details of the new features are as follows:
Generics Phase 1
Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset. This first phase includes support for generic subprograms. Users can now write programs which declare a generic subprogram, then instantiate and call the instantiations. The SPARK toolset has been significantly updated to provide flow analysis and proof of VCs generated from the first phase subset of generics, although analysis of the generic subprogram body itself will be added in the next phase. Two new documents have been added to the user documentation set for
generics. "SPARK Generics - A user view" describes a subset of Ada Generics which is defined for SPARK 95 and onwards whilst maintaining the underlying design principles of SPARK. A more concise specification of SPARK generics is given in the "SPARK Generics LRM". The motivation for incorporating generics into SPARK is - as with Ada - to provide the user with reusable components. In SPARK, these can be implemented and proven once but instantiated many times without requiring the implementation of the component to be re-analysed. The introduction of generics will provide a means, in a future release, to provide more SPARK versions of the Ada libraries, in particular the Ada Container Library.
Dynamic Flow Analyser and VCG Heaps
The main Examiner data structures used by the flow-analyser and the verification-condition generator have been re-implemented so they now extend themselves automatically rather than hitting a capacity limit. This means that the user no longer has to select between two statically-sized versions of the Examiner - spark and megaspark. A new debug option "-debug=t" has been implemented that gives more detail when "-statistics" is also selected. This option currently produces a histogram showing the peak usage of each major data structure.
As a result of the internal changes made in implementing this new feature users should also notice a reduction in the time taken to launch the Examiner.
Unicode characters now allowed in string literals
The Examiner now supports string literals containing Unicode characters. This allows, for example, strings containing umlauts, as in Sausage : constant String := "Thüringer Bratwurst";
Improved use of types and subtypes in FDL
It is now becoming increasingly common to use other proof systems such as Alt-Ergo (via SPARKBridge), Isabelle and Riposte to discharge SPARK VCs. It can be very beneficial to these proof systems to have richer type information included in the FDL. Consequently, the Examiner has been modified to produce this information.
This change is backward compatible, so the Simplifier will still accept the generated FDL and discharge VCs as before. Other proof systems can make use of this information to significantly narrow the bounds for variables they reason about.
Improvements to Simplifier tactics and performance
The Simplifier includes new deduction rules and tactics for numeric expressions and VCs that arise from loop statements that iterate over an unconstrained array type. These new rules and tactics will give improved performance from the Simplifier when discharging certain types
Auto-generation of refinement rules
The Examiner will now generate refinement rules for refined own variables alleviating the need for some user rules. This will benefit users performing proofs involving abstract/refined own variables by allowing more VCs to be discharged automatically.
Whilst still an experimental feature, a number of changes have been made to SPARKBridge and support for Victor - a feature that gives access to alternate theorem provers.
- The -solver option for Victor has been extended to allow additional SMT solvers to be used: CVC3, Yices and Z3. Alt-Ergo is still supported and remains the only prover actually shipped with SPARK.
- Victor has been updated to the latest upstream version. The most important new features are support for SMTLIB2 and support for user rules.
- Victor and Alt-Ergo are now shipped and supported for OSX. This expands experimental support for Victor to the main three platforms: Windows, GNU/Linux and OSX.
A new utility has been added to SPARK to clean out files generated by the SPARK tools. By default this tool simply deletes all vcg, rep, lst, siv, sum, etc. files when invoked without arguments. A user manual for SPARKClean is available with the release that provides full documentation of the options available.