We are happy to announce a new release of Why3, version 1.3.0, available
from the Web page http://why3.lri.fr/
There have been numerous changes since the last release (see below for a
list). Here are some of the most important ones.
- Module cloning now has much stricter requirements; this fixes the last
remaining causes of unsoundness of Why3, as far as we know.
- Finite sets and maps have been reworked in the standard library.
- Preliminary support has been added for strings in WhyML and in the
standard library.
- Performances have been considerably improved; this should be especially
noticeable on huge proof sessions.
Changes between 1.2.1 and 1.3.0 are as follows:
(:x: marks a potential source of incompatibility)
Standard library
* `pqueue.Pqueue` is now modeled using sequences instead of lists :x:
* `queue.Queue` is now modeled using sequences instead of lists :x:
* the `set` library has been revamped :x:
- in `set.Fset`, type `set` becomes `fset`; `choose` becomes `pick`
- module `appset.Appset` becomes `set.SetApp`;
`impset.Impset` becomes `set.SetImp`
- in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
* new library `fmap` for finite maps
- `Fmap`: polymorphic, logic finite maps to be used in logic
- `MapApp`, `MapAppInt`, `MapImp`, `MapImpInt`: monomorphic finite maps to
be used in programs
* no more libraries `appmap` and `impmap` :x:
* no more library `sum.Sum` (subsumed by `int.Sum`) :x:
* new library `string` for character strings
- `String`: basic string operations
- `OCaml`: additional operations dedicated to extraction to OCaml
- `RegExpr`: regular expressions
Language
* the type `string` is a new built-in type; string literals can be
given between double-quotes; see manual, Section 7.1 :x:
* it is now possible to give a name to preconditions and assertions;
`requires Foo { a = 3 }` sets the attribute `[@hyp_name:Foo]`, which tries
to give the name `Foo` to the corresponding hypothesis after introduction
* identifiers used for specification (resp. definition) of a function `foo`
have been renamed from `foo_spec` (resp. `foo_def`) to `foo'spec` (resp.
`foo'def`) :x:
* identifiers used for goals `VC foo` have been renamed to `foo'vc`
* identifiers used for record constructor `mk foo` have been renamed to
`foo'mk` :x:
* the `alias` clause can now be used in program functions to force the
aliasing
of function parameters and/or named returns
Tools
* counterexamples given by `why3prove` are no longer printed using JSON
by default; pass option `--json` to restore the previous behavior
* new tool `why3pp` to pretty print Why3 source code (inductive definitions
to LaTeX,
formatting of mlw files)
Documentation
* improved Chapter 7 on the WhyML language (record types, various
kinds of function declarations, module cloning, etc.)
* improved Section 11.4 on drivers, including an automatically generated
dependency graph of driver files
* improved Section 11.5 on transformations, including transformations
with arguments
API
* `Call_provers.print_prover_result` now takes an additional argument
`~json_model` to indicate whether counterexamples are printed using JSON :x:
* indices of array are now `model_value` for counterexamples :x:
* ITP constructor `Task` now contains the location of the goal :x:
* ITP constructor `Source_and_ce` has now 3 arguments instead of 2 :x:
* ITP constructors `File_contents` and `Source_and_ce` has a new argument for
the file format :x:
* ITP constructor `File_contents` has a new boolean argument for
interpretation of the file in the IDE as `read_only` :x:
* new ITP constructor `Ident_notif_loc` :x:
* ITP constructor `Get_first_unproven_node` now takes a heuristic name
argument :x:
Transformations
* `apply` and `rewrite` now behave better in presence of `let`;
hypotheses with nested let-bindings can now be applied :x:
* passing arguments to argument-free transformations is now forbidden
(previously ignored) :x:
* passing too many arguments to a transformation does not display a popup
anymore
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
* `destruct` now destructs `not p` into `p -> false`;
`destruct_rec` can further destruct afterwards;
`destruct` can also destruct `true` and `false` :x:
* decision procedures used for reflection must now be declared explicitly
using
`meta reflection val foo` :x:
* `remove` and `bisect` should not raise unnecessary popups anymore
* added `remove_rec`
* attribute `inline:trivial` can be put on definitions to force their
inlining by the transformation `inline_trivial`
IDE
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
* added a "reset proofs" command in the Tools menu to remove all the proofs
from the session
* default proof strategies "Auto level 1" and "Auto level 2"
have been respectively renamed "Auto level 2" and "Auto level 3";
"Auto level 1" now behaves similarly to "Auto level 0" but with a longer
time limit; more details in the manual, Section 10.6 "Proof Strategies" :x:
* strategies can now be defined using `%t` (resp. `%m`) to call a prover with
the default timelimit (resp. memlimit)
* added minimal search menu
* a merlin-like feature to find the identifier located under the cursor has
been
added in the Edit menu.
* read-only files can now be displayed and removed by right-clicking on their
tab titles
* colors for error can now be edited in why3.conf more precisely
* most of the preferences can now be changed for the current session
* Ctrl-Down/Ctrl-Up are mapped to more straightforward moves; the former
movements can be triggered with Ctrl-Left/Ctrl-Right
Realizations
* added experimental realizations for new Set theories in both Isabelle and
Coq
Provers
* support for Alt-Ergo 2.3.1 (released Feb 19, 2020)
* support for Vampire 4.2.2 (released Dec 14, 2017)
* support for Coq 8.10.0 (released Oct 8, 2019)
* support for Coq 8.10.1 (released Oct 25, 2019)
* support for Coq 8.10.2 (released Oct 29, 2019)
* support for Coq 8.11.0 (released Jan 30, 2020)
* make use of built-in support for strings by Z3 (4.8.6), and CVC4 (1.7)
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
