A new release of Why3, version 0.87.0, is available from the web page
http://why3.lri.fr/ ; OPAM packages for this version of Why3 should soon
be available.
There are no major changes in this release. It mainly provides support
for new versions of provers. There are also some improvements to the
bitvector theory and to the family of "split" transformations. Finally,
translation to SMT-LIB has been improved for tasks containing no
polymorphic symbols. See the detailed list of changes below.
Guillaume, for the Why3 team
Language
* Add new logical connectives "by" and "so" as keywords
Tools
o add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available
for why3 commands "prove" and "ide".)
* removed "jstree" style from the "session" command
Transformations
* All split transformations respect the "stop_split" label now.
split_*_wp is a synonym for split_*_right
* split_*_right split the left-hand side subformulas
when they carry the "case_split" label
* split_intro is now the composition of split_goal_right and
introduce_premises
Library
* improved bitvector theories
API
* Renamed functions in Split_goal
* split_intro moved to Introduction
Encodings
* When a task has no polymorphic object (except for the special
cases of equality and maps) then the translation to SMT-LIB
format is direct
Provers
* discarded support for Alt-Ergo versions older than 0.95.2
o support for Alt-Ergo 1.01 (released Feb 16, 2016) and
non-free versions 1.10 and 1.20
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Coq 8.5 (released Jan 21, 2016)
o support for Gappa 1.2.0 (released May 19, 2015)
* discarded support for Isabelle 2014
o support for Isabelle 2015 (released May 25, 2015) and
Isabelle 2016 (released Feb 17, 2016)
o support for Z3 4.4.0 (released Apr 29, 2015) and
4.4.1 (released Oct 5, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Distribution
* non-free files have been removed: "boomy" icon set,
javascript helpers for "why3 session html --style jstree"
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
