SPARK Pro 20.x
- Support for pointers through ownership
- Support for volatile variables to prevent compiler optimizations
- Contracts added to Ada Standard Library
- Improved floating-point support in Alt-Ergo prover
- Better support for recursive functions
- Parallel analysis of subprograms
- Better messages from flow analysis
- Dead code detected by proof warnings
- Unproved parts of preconditions identified
- Automatic target configuration for GNAT runtimes
- Ability to specify file-specific switches
See the full SPARK 20 Release notes »
SPARK Pro 19.x
- Support for more fixed-point types and operations
- New lemmas for exponentiation, fixed-point arithmetic and higher-order functions
- Automatic detection of array initialization with non-static bounds
- Improved support for floating-point computations
- Explanation part in messages to investigate unproved checks
- Warnings issued by proof to detect inconsistencies
- Counterexamples on individual paths through subprograms
- Possibility to run analysis on region of code in GPS
- New Analysis Report panel in GPS
- Speedup on large projects
See the full SPARK 19 Release notes »
SPARK Pro 18.x
- Easier program specification
- Preconditions on standard numerical functions
- Contracts on formal containers
- Specification of subprogram termination
- Greater proof automation
- Better integration of CodePeer engine as additional prover
- Unrolling of simple for-loops
- Enhanced library of lemmas for floating-point arithmetic
- Ability to perform interactive proof in GPS
- Easier tool configuration with cross runtimes
- Support for caching using memcached
See the full SPARK 18 Release notes »
SPARK Pro 17.x
- Improved proof automation
- CodePeer engine available as an additional prover
- Generation of loop invariants for frame conditions
- Library of lemmas for non-linear arithmetic
- Finer granularity in proof of conjunctions
- Improved proof interaction
- Improved counterexamples (arrays, quantifiers, enumerations)
- New mode statistics for proof results
- Display mode for proof
- Replay mode for proof
- Support for type invariants