Fedora 21 Update: why3-0.85-2.fc21

updates at fedoraproject.org updates at fedoraproject.org
Tue Sep 23 04:33:29 UTC 2014

Fedora Update Notification
2014-09-10 01:58:20

Name        : why3
Product     : Fedora 21
Version     : 0.85
Release     : 2.fc21
URL         : http://why3.lri.fr/
Summary     : Software verification platform
Description :
Why3 is the next generation of the Why software verification platform.
Why3 clearly separates the purely logical specification part from
generation of verification conditions for programs.  It features a rich
library of proof task transformations that can be chained to produce a
suitable input for a large set of theorem provers, including SMT
solvers, TPTP provers, as well as interactive proof assistants.

Update Information:

This update removes an obsolete ExcludeArch tag from ocaml-zip.  Besides ocaml-zip, flocq and why3, the other updates are just rebuilds due to the updated packages.

Changes in flocq 2.4.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
- added theorems about double rounding being innocuous (Fappli_double_round.v)
- improved a bit the efficiency of IEEE-754 arithmetic

Changes in why3 0.84:

- file generated by "why3session html f.mlw" is now "f/why3session.html" and not "f/f.html"
- the default behavior of why3 has been moved to the "prove" subcommand
- options --exec, --extract, and --realize, have been moved to subcommands: execute, extract, and realize
- why3replayer has been moved to the "replay" subcommand
- other tools have been moved to why3 subcommands too: config, doc, ide, session, wc; for local usage, the old commands are still available

Proof sessions:
- session files are split in two parts: "why3session.xml" and "why3shapes". The latter file contains the checksums and the shapes for the goals. That second file is not strictly needed for replaying a proof session, it is only useful when input programs are modified, to track obsolete goals. If Why3 is compiled with compression support (provided by ocamlzip library) then files for shapes are compressed into why3shapes.gz.

- renamed array.ArraySorted -> array.IntArraySorted. array.ArraySorted is now generic, with type and order relation parameters
- reduced amount of "use export" in the standard library: theories now only export the symbols they define. Users may need to insert more "use import" in their theories (typically int.Int, option.Option, list.List, etc.).

- fixed Coq printer (former Coq proofs may have to be updated, by removing non-emptiness constraints from polymorphic type applications)
- support for Coq8.4pl4
- support for Isabelle2014
- support for CVC4 1.4
- updated support for TPTP TFA syntax (used by provers Beagle and Princess)

- new transformation "compute_in_goal" that simplifies the goal, by computation, as much as possible

Changes in why3 0.85:

- 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

- use the full path of identifiers when the user introduces namespaces (BTS #17181)

- fix a soundness bug in "compute_in_goal" regarding the handling of logical implication.
- 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
- new transformation "compute_specified":
    - less aggressive variant of "compute_in_goal"
    - Unfolding of definitions is controlled using meta "rewrite_def"
- fixed a bug in "eliminate_if" when applied on inductive definitions

- fixed wrong warning when detecting Isabelle2014


This update can be installed with the "yum" update program.  Use
su -c 'yum update why3' at the command line.
For more information, refer to "Managing Software with yum",
available at http://docs.fedoraproject.org/yum/.

All packages are signed with the Fedora Project GPG key.  More details on the
GPG keys used by the Fedora Project can be found at

More information about the package-announce mailing list