[Why3-club] New release 1.2.0

Guillaume Melquiond guillaume.melquiond at inria.fr
Mon Feb 11 17:12:26 CET 2019


We are happy to announce a new release of Why3, version 1.2.0, available 
from the Web page http://why3.lri.fr/


One of the major changes is that WhyML now offers some "let ref" 
syntactic sugar to make references look like plain variables, e.g.,

   let rec f91_tco (n0: int) : int
   = let ref n = n0 in
     while n <= 100 do
       variant { 101 - n }
       n <- f91_tco (n + 11)
     done;
     n - 10


Changes between 1.1.1 and 1.2.0 are as follows:
(:x: marks a potential source of incompatibility)

Session
   * file path stored in session files are now represented in a
     system-independent way

Drivers
   * the clause `syntax converter` has been removed; any former use
     should be replaced by `syntax literal` and/or `syntax function` :x:

Language
   * the `any` expression is now always ghost :x:
   * a syntactic sugar called "auto-dereference" is introduced, so as
     to avoid, on simple programs, the heavy use of `(!)` character on
     references; see details in Section A.1 of the manual

Transformations
   * `split_vc` and `subst_all` now avoid substituting user symbols by
     generated ones :x:
   * `destruct_rec` applies `destruct` recursively on a goal
   * `destruct` now simplifies away equalities on constructors :x:
   * `destruct` now simplifies `if .. then .. else ..` and
     `match .. with ..` :x:
   * `destruct_alg` renamed to `destruct_term`; it also has a new
     experimental keyword `using` to name newly destructed elements :x:

Tools
   * added a command `why3 session update` to modify sessions from the
     command line; so far, only option `-rename-file` exists, for
     renaming files
   * `why3 config --add-prover` now takes the shortcut as second
     argument; option `--list-prover-ids` has been renamed to
     `--list-prover-families` :x:

IDE
   * clicking on the status of a failed proof attempt in the proof tree
     now generates counterexamples
   * added support for GTK3

Counterexamples
   * the trigger for counterexamples has been changed; read Section 5.3.7
     of the manual for details :x:
   * various improvements on the generated counterexamples
   * field names now use ident names instead of smt generated ones, e.g.,
     `int32qtint` -> `int32'int` :x:
   * fixed parsing of bitvector values from counterexamples generated
     by Z3

Extraction
   * fixed extraction of functions passed as arguments
   * fixed extraction of recursive polymorphic functions for Ocaml
   * improved extraction of records for C

Standard library
   * `Stack.length` and `Queue.length` now return a `Peano.t`, for
     improved extraction :x:

Provers
   * support for Z3 4.8.1 (released Oct 16, 2018)
   * support for Z3 4.8.3 (released Nov 20, 2018)
   * support for Z3 4.8.4 (released Dec 20, 2018)
   * support for Coq 8.9.0 (released Jan 17, 2019)
   * upgraded Coq realizations for floating-point arithmetic to Flocq 3.1


More information about the Why3-club mailing list