[Why3-club] New release 1.0.0

Guillaume Melquiond guillaume.melquiond at inria.fr
Mon Jun 25 11:36:26 CEST 2018


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`


More information about the Why3-club mailing list