[Why3-club] New release Why3 0.83

Claude Marche Claude.Marche at inria.fr
Fri Mar 14 19:09:44 CET 2014

A new release of Why3, version 0.83, is available from the Web page

A detailed list of changes is given below.

- Claude, for the Why3 team

  o extra semicolons are now allowed at end of blocks
  o new clause "diverges". Loops and recursive calls not annotated
    with variants will generate a warning, unless the "diverges"
    clause is given
  o clauses "reads" and "writes" now accept an empty set
  * modified syntax for "abstract": abstract <spec> <expr> end
  o types in quantifiers are now optional
  o formulas and Boolean terms can be used interchangeably

  * [fix] removed inconsistency in libraries map.MapPermut and
  * names, definitions, and meaning of symbols "permut..." have
    been modified

  o new version of prover: Coq 8.4pl3
  o new version of prover: Gappa 1.1.0
  o new version of prover: E prover 1.8
  * Coq 8.3 is no longer supported
  o improved support for Isabelle2013-2

  o new option --exec to interpret WhyML programs; see doc chapter 8
  o new option --extract to compile WhyML programs to OCaml;
    see doc chapter 8 and modules/mach/{int,array}.mlw
  * [why3replayer] renamed option -obsolete-only to --obsolete-only,
    -smoke-detector to --smoke-detector, -force to --force
  * [why3replayer] replay now fails if new goals are added

  o new type-inferring API for logical terms and program expressions

bug fixes
  o fixed compilation bug with lablgtk 2.18
  * fixed Coq printer (former Coq proofs may have to be updated, with
    extra qualification of imported symbols)

More information about the Why3-club mailing list