Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Project Filelist for Why3

File Release Notes and Changelog

Release Name: 0.80

Release Notes
Programs:
  o new concrete syntax for programs
  o new API for programs
  o type invariants
  o ghost code

Transformations:
  o induction (experimental, undocumented)
  o bisection (experimental, undocumented)

Provers support:
  o support for Coq 8.4
  o dropped support for Coq 8.2
  o support for forthcoming PVS 6.0, including realizations
  o support for iProver and Zenon

Misc:
  o improved output of "why3session latex"
    (incompatible changes in LaTeX macros)
  o [replayer] new option -q for running quietly
  o a warning is emitted for unused bound logic variables in "forall",
    "exists" and "let"
  o a warning is emitted for any occurrence of a formula of the form
    "exists x, P -> Q". Formulas of this form are usually a user
    mistake. If this is intended, one can write "exists x, not P \/ Q"
    instead

Bug fixes:
  o Coq output uses type classes to ensure Why3 types are inhabited
  o fixed bug on merging config files which prevented the use
    of Why3 back-end of the Frama-C/Jessie plugin when Coq is
    not installed. (Bug 14672 of the Bug Tracking System)
  o fixed bugs 13503 and 13375 of the Bug Tracking System
Change Log
  * [whyml] modified syntax for mlw programs; a summary of changes is
    given in Appendix A of the manual
  o [whyml] support for type invariants and ghost code
  o [api] Ocaml interfaces for constructing program modules
  o [transformation] experimental support for induction on integers
    and on algebraic types
  o [interface] new system of warnings, that includes:
     - form "exists x, P -> Q", likely an error
     - unused bound logic variables in "forall", "exists" and "let"
  o [replayer] new option -q, for running quietly
  * [session] improved output of "why3session latex"; LaTeX macros have
    more arguments
  o [prover] support for Coq 8.4
  * [prover] dropped support for Coq 8.2
  o [prover] support for forthcoming PVS 6.0, including realizations
  o [prover] support for iProver and Zenon
  o [prover] new output scheme for Coq using type classes, to ensures
    types are inhabited
  * [driver] theory realizations now use meta "realized_theory" instead
    of "realized"
  * [config] modifiers in --extra-config are now called [prover_modifier]
    instead of just [prover]