A new release of Why3, version 0.84, is available from the Web page
http://why3.lri.fr.
This is mainly a bug-fix release, in particular to fix two soundness
bugs, as detailed in the changes below
- Claude, for the Why3 team
langage
* fix a soundness bug in the detection of aliases when calling a
WhyML function: some alias could have been forgotten when a type
variable was substituted with a mutable type
sessions
o use the full path of identifiers when the user introduces namespaces
(BTS #17181)
transformations
* fix a soundness bug in "compute_in_goal" regarding the handling of
logical implication.
o several improvements to "compute_in_goal":
. left-hand side of rewrite rules can be any symbols, not only
non-interpreted ones.
. perform beta-reduction when possible
. the maximal number of reduction steps can be increased using meta
"compute_max_steps"
. the transformation is documented in details in the manual
o new transformation "compute_specified":
less aggressive variant of "compute_in_goal".
Unfolding of definitions is controlled using meta "rewrite_def".
o fixed a bug in "eliminate_if" when applied on inductive definitions
provers
o fixed wrong warning when detecting Isabelle2014
--
Claude Marché | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex |
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
