Development Log

  • SPARK Pro
    Mar 22nd, 2016

    Use stable names for aggregates used in definitions
    Aggregates used as initialization expressions in the declaration of objects now get transformed in Why3 into modules and functions with a stable name across versions in GNATprove, based on the name of the object they define. This eases maintenance of manual proofs done in interactive provers.