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

See the full SPARK 18 Release notes »