Fedora 21 Update: why-2.34-10.fc21

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


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

Name        : why
Product     : Fedora 21
Version     : 2.34
Release     : 10.fc21
URL         : http://why.lri.fr/
Summary     : Software verification platform
Description :
Why is a software verification platform that applies formal proving
tools to annotated programs.  It is currently capable of analysis of C
(through "Frama-C"), Java (through the included tool "Krakatoa"), and
potentially ML programs with some modification into Why's own ML-like
language.  Furthermore, Why is capable of analysis of any program that
is mapped onto its own internal language.  It uses a weakest
precondition involving calculus to generate potential theorems necessary
for the proof of a program's correctness.  It translates these theorems
into formats that can be used by external proof assistants (without any
extra work Coq, PVS, HOL Light, and Mizar are supported - having one is
recommended and both Coq and PVS are packaged for Fedora) and automated
theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3,
CVC3, and Zenon are supported and Alt-Ergo, CVC3, and Zenon are packaged
for Fedora) so that these results can be externally proven, resulting in
a proof of program correctness.

Note: Each user account must be set up by running "why-config" at the
command line (to set up a configuration file).

--------------------------------------------------------------------------------
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:

Tools:
- 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.

Library:
- 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.).

Provers:
- 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)

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

Changes in why3 0.85:

Language:
- 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

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

Transformations:
- 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

Provers:
- fixed wrong warning when detecting Isabelle2014

--------------------------------------------------------------------------------

This update can be installed with the "yum" update program.  Use
su -c 'yum update why' 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
https://fedoraproject.org/keys
--------------------------------------------------------------------------------


More information about the package-announce mailing list