We are happy to announce a new major release of Why3, version 1.00,
available from the Web page http://why3.lri.fr/.
The detailed changes are listed below. The two major changes of this
release with respect to the former release 0.88.3 concern:
1) the WhyML programming language and the associated VC generator
2) the user interface why3ide.
1) Concerning the WhyML language, the main change is a stricter and
clearer distinction on which functions can be used in the logic and/or
in programs. A consequence is that some work is required for porting
WhyML sources from the former syntax to the new one; in particular,
functions to be used both in logic and programs should be declared with
a 'let function' declaration. A quick migration guide is given in
Appendix A.1 of the manual (page 109 of the PDF manual). An important
consequence of these changes is that former axiomatic definitions of
logic functions can now use pre- and post-conditions, and also variants
for recursive logic functions.
2) Concerning the graphical interface, the most visible changes are
first the disappearance of the toolbar on the left of the window,
replaced by a contextual menu that shows up when clicking the right
mouse button on any row of the session tree, and second a new text input
field where textual commands can be entered. This text-based interface
allows one to interact with proof tasks by using proof transformations
that take user arguments. Note also that the new interface makes it
possible to directly edit the Why3 source files within the IDE.
Do not hesitate to provide any feedback on this new major release,
either by messages on this list or by using the ticket system
https://gitlab.inria.fr/why3/why3/issues. Note that the documentation is
not yet fully up-to-date; it will be updated in the coming weeks.
The OPAM packages are in the process of being released. Note that the
'why3' package no longer contains the whole system; install the
'why3-ide' package for the graphical user interface, as well as the
'why3-coq' package if you need the Coq realizations.
Here is a more comprehensive list of changes:
Core
* improved support of counter-examples
* attribute `[@vc:sp]` on an expression switches from traditional WP
to Flanagan-Saxe-like VC generation
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any
more, so equality functions must be declared/defined on a per-type
basis (already done for type `int` in the standard library) :x:
Language
* numerous changes to syntax, see documentation appendix :x:
* `let function`, `let predicate`, `val function`, and `val predicate`
introduce symbols in both logic and programs
* added overloading of program symbols
* new contract clause `alias { <term> with <term>, ... }` :x:
* support for parallel assignment `<term>,... <- <term>,...`
* support for local exceptions using `exception ... in ...`
* added `break`, `continue`, and `return` statements
* support for `exception` branches in `match` constructs
* support for `for` loops on range types
(including machine integers from the standard library)
* support for type coercions in logic using `meta coercion`
* keyword `theory` is deprecated; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x:
* cloned axioms turn into lemmas; use `with axiom my_axiom`
or `with axiom .` to keep them as axioms :x:
* `any <type> <spec>` produces an existential precondition;
use `val f : <type> <spec> in ...` (unsafe!) instead :x:
* `use T` and `clone T` now import the generated namespace T;
use `use T as T` and `clone T as T` to prevent this :x:
* `pure { <term> }` produces a ghost value in program code
Standard library
* machine integers in `mach.int.*` are now range types :x:
* added a minimal memory model for the C language in `mach.c`
Extraction
* improved extraction to OCaml
* added partial extraction to C using the memory model of `mach.c`
* added extraction to CakeML (using `why3 extract -D cakeml ...`)
Transformations
* transformations can now have arguments
* added transformations `assert`, `apply`, `cut`, `rewrite`, etc.,
à la Coq
* added transformations for reflection-based proofs
Drivers
* support for `use` in theory drivers
IDE
* replaced left toolbar by a contextual menu
* source is now editable
* premises are no longer implicitly introduced
* added textual interface to call transformations and provers
Tools
* deprecated `.why` file extension; use `.mlw` instead
Provers
* removed the `why3` Coq tactic :x:
* dropped support for Coq 8.4 :x:
Miscellaneous
* moved the opam base package to `why3`; added `why3-ide` and
`why3-coq`
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
