[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
http://why3.lri.fr.

A detailed list of changes is given below.

- Claude, for the Why3 team

syntax
  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

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

provers
  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

tools
  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

API
  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