SPARK Pro 18.1

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