| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: why | Distribution: Fedora Project |
| Version: 2.29 | Vendor: Fedora Project |
| Release: 2.fc15 | Build date: Thu Jul 14 22:59:04 2011 |
| Group: Applications/Engineering | Build host: x86-14.phx2.fedoraproject.org |
| Size: 10985049 | Source RPM: why-2.29-2.fc15.src.rpm |
| Packager: Fedora Project | |
| Url: http://why.lri.fr/ | |
| Summary: Software verification platform | |
Why is a software verification platform that applies formal proving tools to annotated programs. It is currently capable of analysis of C (through the included tool "Caduceus"), 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).
LPGLv2 with exceptions
* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
- Fix broken conditionals
* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 2.29-1
- New upstream release (fixes FTBFS: bz 715902)
- Remove unnecessary spec file elements (BuildRoot, etc.)
- Update approach to filtering provides and requires
- Add has_pvs analogously to has_coq, and simplify macro usage
- Add (X)Emacs support packages
- New subpackage for the jessie plugin to avoid unowned directories and
permit a direct dependency on frama-c
- Prepare for the eventual availability of APRON
* Thu Apr 14 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.2
- add ppc to excludearch, too. No pvs-sbcl available there
* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
- add ppc64 to excludearch, no sbcl available there
* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.28-1
- Since 2.26 FTBFS, try latest upstream (2.28).
- Rebase Makefile.in patch.
- Fix(?) test result.
- No libdir/frama-c directory is created any more.
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.26-2
- Bump and rebuild for OCaml 3.12.
* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 2.26-1
- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
- Integrated with Frama-C and PVS (as pvs-sbcl)
* Mon Jan 11 2010 Richard W.M. Jones <rjones@gmail.com> - 2.23-2
- Rebuild to fix dependencies.
* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 2.23-1
- Upgrade to upstream version 2.23
- Move execstack fixing to spec file from patch
- Moved patch descriptions to initial patch declaration as in examples
in Fedora documentation
- New Caduceus, Krakatoa documentation
- Update test result from small test min.mlw
- Added CVC3 interfacing capabilities
- Removed patch for gwhy configuration, as there is a new mechanism for this
* Tue Sep 22 2009 Dennis Gilmore <dennis@ausil.us> - 2.17-5
- Exclude sparc64 s390 s390x there is no ocaml there
* Fri Aug 07 2009 Alan Dunn <amdunn@gmail.com> - 2.17-4
- Removed now irrelevant check for no OCaml in Fedora < 9 (those
distributions are EOL)
- Changed ExcludeArch to proper Fedora versions
- Builds coq subpackage exactly when Coq can be built, thus making
build independent of whether Coq can be built
- define -> global
- Fixed accidental use of in tar ocamlgraph instead of one that is
separately packaged
* Mon Jul 27 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 2.17-1
- Upgrade to version 2.17 (bz: 477790)
- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
- Minor filename change in 2.17 (GPL -> LICENSE)
- Added back Coq .v files to match policy for Coq
- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
- Minor changes to patches to ensure they still work in 2.17
- Corrected package location gwhy-icon.png (should only be in gwhy)
* Tue Aug 05 2008 Alan Dunn <amdunn@gmail.com> 2.14-2.1
- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
* Fri Aug 01 2008 Alan Dunn <amdunn@gmail.com> 2.14-2
- Fixed minor issues in response to package review:
- Inclusion of COPYING, GPL license-related files
- Added config.mll patch to make default config file created nicer
- Changes subpackage dependencies to be fully versioned.
- Makes during build allowed to be noisy (allowed to print).
* Wed Jul 30 2008 Alan Dunn <amdunn@gmail.com> 2.14-1
- Changed to new version of why, removed previous why-cpulimit name
change, zenon output format patches as the issues were fixed in
why 2.14.
- Moved doc subpackage back into main package.
- Added example files to documentation subpackage.
- Added check section with test on small why file.
- Reformatted some macro names for greater readability.
* Thu Jul 24 2008 Alan Dunn <amdunn@gmail.com> 2.13-2
- Added several patches: fixed Zenon output, completed fix of rename
of cpulimit -> why-cpulimit.
* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
- Initial Fedora RPM version.
/usr/bin/caduceus /usr/bin/krakatoa /usr/bin/rv_merge /usr/bin/simplify2why /usr/bin/tool-stat /usr/bin/why /usr/bin/why-config /usr/bin/why-cpulimit /usr/bin/why-dp /usr/bin/why-obfuscator /usr/bin/why-stat /usr/bin/why2html /usr/lib/caduceus /usr/lib/caduceus/harvey /usr/lib/caduceus/harvey/caduceus_why.rv /usr/lib/caduceus/isabelle /usr/lib/caduceus/isabelle/caduceus_why.thy /usr/lib/caduceus/why /usr/lib/caduceus/why/caduceus.why /usr/lib/caduceus/why/caduceus_arith.why /usr/lib/why /usr/lib/why/images /usr/lib/why/images/accept32.png /usr/lib/why/images/bug32.png /usr/lib/why/images/clock32.png /usr/lib/why/images/delete32.png /usr/lib/why/images/help32.png /usr/lib/why/images/logo-why-small.png /usr/lib/why/images/pause32.png /usr/lib/why/images/play32.png /usr/lib/why/images/stop32.png /usr/lib/why/images/why-logo-1.png /usr/lib/why/java_api /usr/lib/why/java_api/java /usr/lib/why/java_api/java/io /usr/lib/why/java_api/java/io/BufferedWriter.java /usr/lib/why/java_api/java/io/File.java /usr/lib/why/java_api/java/io/FileDescriptor.java /usr/lib/why/java_api/java/io/FileNotFoundException.java /usr/lib/why/java_api/java/io/FileReader.java /usr/lib/why/java_api/java/io/FilterOutputStream.java /usr/lib/why/java_api/java/io/IOException.java /usr/lib/why/java_api/java/io/InputStream.java /usr/lib/why/java_api/java/io/InputStreamReader.java /usr/lib/why/java_api/java/io/ObjectStreamClass.java /usr/lib/why/java_api/java/io/OutputStream.java /usr/lib/why/java_api/java/io/OutputStreamWriter.java /usr/lib/why/java_api/java/io/PrintStream.java /usr/lib/why/java_api/java/io/Reader.java /usr/lib/why/java_api/java/io/Serializable.java /usr/lib/why/java_api/java/io/StreamTokenizer.java /usr/lib/why/java_api/java/lang /usr/lib/why/java_api/java/lang/ArrayStoreException.java /usr/lib/why/java_api/java/lang/CharSequence.java /usr/lib/why/java_api/java/lang/Character.java /usr/lib/why/java_api/java/lang/Class.java /usr/lib/why/java_api/java/lang/Cloneable.java /usr/lib/why/java_api/java/lang/Comparable.java /usr/lib/why/java_api/java/lang/Double.java /usr/lib/why/java_api/java/lang/Exception.java /usr/lib/why/java_api/java/lang/IllegalArgumentException.java /usr/lib/why/java_api/java/lang/Integer.java /usr/lib/why/java_api/java/lang/Long.java /usr/lib/why/java_api/java/lang/Math.java /usr/lib/why/java_api/java/lang/Number.java /usr/lib/why/java_api/java/lang/NumberFormatException.java /usr/lib/why/java_api/java/lang/Object.java /usr/lib/why/java_api/java/lang/RuntimeException.java /usr/lib/why/java_api/java/lang/String.java /usr/lib/why/java_api/java/lang/StringBuffer.java /usr/lib/why/java_api/java/lang/System.java /usr/lib/why/java_api/java/lang/Throwable.java /usr/lib/why/java_api/java/util /usr/lib/why/java_api/java/util/AbstractMap.java /usr/lib/why/java_api/java/util/Collection.java /usr/lib/why/java_api/java/util/HashMap.java /usr/lib/why/java_api/java/util/HashMapIntegerInteger.java /usr/lib/why/java_api/java/util/HashMapIntegerLong.java /usr/lib/why/java_api/java/util/Iterator.java /usr/lib/why/java_api/java/util/Locale.java /usr/lib/why/java_api/java/util/Map.java /usr/lib/why/java_api/java/util/Set.java /usr/lib/why/javacard_api /usr/lib/why/javacard_api/com /usr/lib/why/javacard_api/com/sun /usr/lib/why/javacard_api/com/sun/javacard /usr/lib/why/javacard_api/com/sun/javacard/impl /usr/lib/why/javacard_api/com/sun/javacard/impl/Constants.java /usr/lib/why/javacard_api/com/sun/javacard/impl/NativeMethods.java /usr/lib/why/javacard_api/com/sun/javacard/impl/PackedBoolean.java /usr/lib/why/javacard_api/com/sun/javacard/impl/PrivAccess.java /usr/lib/why/javacard_api/java /usr/lib/why/javacard_api/java/lang /usr/lib/why/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java /usr/lib/why/javacard_api/java/lang/Exception.java /usr/lib/why/javacard_api/java/lang/IndexOutOfBoundsException.java /usr/lib/why/javacard_api/java/lang/Object.java /usr/lib/why/javacard_api/java/lang/RuntimeException.java /usr/lib/why/javacard_api/java/lang/Throwable.java /usr/lib/why/javacard_api/javacard /usr/lib/why/javacard_api/javacard/framework /usr/lib/why/javacard_api/javacard/framework/AID.java /usr/lib/why/javacard_api/javacard/framework/APDU.java /usr/lib/why/javacard_api/javacard/framework/APDUException.java /usr/lib/why/javacard_api/javacard/framework/Applet.java /usr/lib/why/javacard_api/javacard/framework/CardException.java /usr/lib/why/javacard_api/javacard/framework/CardRuntimeException.java /usr/lib/why/javacard_api/javacard/framework/Dispatcher.java /usr/lib/why/javacard_api/javacard/framework/ISO7816.java /usr/lib/why/javacard_api/javacard/framework/ISOException.java /usr/lib/why/javacard_api/javacard/framework/JCSystem.java /usr/lib/why/javacard_api/javacard/framework/OwnerPIN.java /usr/lib/why/javacard_api/javacard/framework/PIN.java /usr/lib/why/javacard_api/javacard/framework/PINException.java /usr/lib/why/javacard_api/javacard/framework/Shareable.java /usr/lib/why/javacard_api/javacard/framework/SystemException.java /usr/lib/why/javacard_api/javacard/framework/TransactionException.java /usr/lib/why/javacard_api/javacard/framework/UserException.java /usr/lib/why/javacard_api/javacard/framework/Util.java /usr/lib/why/javacard_api/javacard/security /usr/lib/why/javacard_api/javacard/security/CryptoException.java /usr/lib/why/javacard_api/javacard/security/DESKey.java /usr/lib/why/javacard_api/javacard/security/DSAKey.java /usr/lib/why/javacard_api/javacard/security/DSAPrivateKey.java /usr/lib/why/javacard_api/javacard/security/DSAPublicKey.java /usr/lib/why/javacard_api/javacard/security/Key.java /usr/lib/why/javacard_api/javacard/security/KeyBuilder.java /usr/lib/why/javacard_api/javacard/security/KeyPair.java /usr/lib/why/javacard_api/javacard/security/MessageDigest.java /usr/lib/why/javacard_api/javacard/security/PrivateKey.java /usr/lib/why/javacard_api/javacard/security/PublicKey.java /usr/lib/why/javacard_api/javacard/security/RSAPrivateCrtKey.java /usr/lib/why/javacard_api/javacard/security/RSAPrivateKey.java /usr/lib/why/javacard_api/javacard/security/RSAPublicKey.java /usr/lib/why/javacard_api/javacard/security/RandomData.java /usr/lib/why/javacard_api/javacard/security/SecretKey.java /usr/lib/why/javacard_api/javacard/security/Signature.java /usr/lib/why/javacard_api/javacardx /usr/lib/why/javacard_api/javacardx/crypto /usr/lib/why/javacard_api/javacardx/crypto/Cipher.java /usr/lib/why/why /usr/lib/why/why/arrays.why /usr/lib/why/why/bool.why /usr/lib/why/why/divisions.why /usr/lib/why/why/floats_common.why /usr/lib/why/why/floats_full.why /usr/lib/why/why/floats_multi_rounding.why /usr/lib/why/why/floats_strict.why /usr/lib/why/why/integer.why /usr/lib/why/why/jessie.why /usr/lib/why/why/jessie_bitvectors.why /usr/lib/why/why/mix.why /usr/lib/why/why/mybag.why /usr/lib/why/why/prelude.why /usr/lib/why/why/real.why /usr/share/doc/why-2.29 /usr/share/doc/why-2.29/CHANGES /usr/share/doc/why-2.29/COPYING /usr/share/doc/why-2.29/LICENSE /usr/share/doc/why-2.29/README /usr/share/doc/why-2.29/README.why /usr/share/doc/why-2.29/Version /usr/share/doc/why-2.29/caduceus.ps /usr/share/doc/why-2.29/examples /usr/share/doc/why-2.29/examples/c /usr/share/doc/why-2.29/examples/c/float /usr/share/doc/why-2.29/examples/c/float/Malcolm.c /usr/share/doc/why-2.29/examples/c/float/Sterbenz.c /usr/share/doc/why-2.29/examples/c/float/Sterbenz2.c /usr/share/doc/why-2.29/examples/c/g4 /usr/share/doc/why-2.29/examples/c/g4/g4.c /usr/share/doc/why-2.29/examples/c/linked-lists /usr/share/doc/why-2.29/examples/c/linked-lists/has_cycle.c /usr/share/doc/why-2.29/examples/c/linked-lists/reverse.c /usr/share/doc/why-2.29/examples/c/linked-lists/search.c /usr/share/doc/why-2.29/examples/c/linked-lists/swap.c /usr/share/doc/why-2.29/examples/c/puf /usr/share/doc/why-2.29/examples/c/puf/parray.c /usr/share/doc/why-2.29/examples/c/puf/parray_frama_c.c /usr/share/doc/why-2.29/examples/c/puf/puf.c /usr/share/doc/why-2.29/examples/c/schorr-waite /usr/share/doc/why-2.29/examples/c/schorr-waite/schorr_waite.c /usr/share/doc/why-2.29/examples/c/sorting /usr/share/doc/why-2.29/examples/c/sorting/quicksort.c /usr/share/doc/why-2.29/examples/c/sorting/selection.c /usr/share/doc/why-2.29/examples/c/trees /usr/share/doc/why-2.29/examples/c/trees/search.c /usr/share/doc/why-2.29/examples/c/tutorial /usr/share/doc/why-2.29/examples/c/tutorial/abs.c /usr/share/doc/why-2.29/examples/c/tutorial/average.c /usr/share/doc/why-2.29/examples/c/tutorial/binary_search.c /usr/share/doc/why-2.29/examples/c/tutorial/flag.c /usr/share/doc/why-2.29/examples/c/tutorial/max.c /usr/share/doc/why-2.29/examples/c/tutorial/modulo.c /usr/share/doc/why-2.29/examples/c/tutorial/purse.c /usr/share/doc/why-2.29/examples/c/tutorial/search.c /usr/share/doc/why-2.29/examples/c/tutorial/swap.c /usr/share/doc/why-2.29/examples/c/ukkonen /usr/share/doc/why-2.29/examples/c/ukkonen/main.c /usr/share/doc/why-2.29/examples/c/ukkonen/ukkonen.c /usr/share/doc/why-2.29/examples/mlw /usr/share/doc/why-2.29/examples/mlw/algo-63-64-65 /usr/share/doc/why-2.29/examples/mlw/algo-63-64-65/algo63.mlw /usr/share/doc/why-2.29/examples/mlw/algo-63-64-65/algo64.mlw /usr/share/doc/why-2.29/examples/mlw/algo-63-64-65/algo65.mlw /usr/share/doc/why-2.29/examples/mlw/binary-search /usr/share/doc/why-2.29/examples/mlw/binary-search/bsearch.mlw /usr/share/doc/why-2.29/examples/mlw/bresenham /usr/share/doc/why-2.29/examples/mlw/bresenham/bresenham.mlw /usr/share/doc/why-2.29/examples/mlw/dijkstra /usr/share/doc/why-2.29/examples/mlw/dijkstra/dijkstra.why /usr/share/doc/why-2.29/examples/mlw/edit-distance /usr/share/doc/why-2.29/examples/mlw/edit-distance/distance.mlw /usr/share/doc/why-2.29/examples/mlw/find /usr/share/doc/why-2.29/examples/mlw/find/find.mlw /usr/share/doc/why-2.29/examples/mlw/heapsort /usr/share/doc/why-2.29/examples/mlw/heapsort/downheap.mlw /usr/share/doc/why-2.29/examples/mlw/heapsort/heapsort.mlw /usr/share/doc/why-2.29/examples/mlw/heapsort/swap.mlw /usr/share/doc/why-2.29/examples/mlw/kmp /usr/share/doc/why-2.29/examples/mlw/kmp/kmp.mlw /usr/share/doc/why-2.29/examples/mlw/linked-lists /usr/share/doc/why-2.29/examples/mlw/linked-lists/length.mlw /usr/share/doc/why-2.29/examples/mlw/linked-lists/rev.mlw /usr/share/doc/why-2.29/examples/mlw/linked-lists/reverse.why /usr/share/doc/why-2.29/examples/mlw/maximumsort /usr/share/doc/why-2.29/examples/mlw/maximumsort/maximumsort.mlw /usr/share/doc/why-2.29/examples/mlw/mergesort /usr/share/doc/why-2.29/examples/mlw/mergesort/mergesort.mlw /usr/share/doc/why-2.29/examples/mlw/mergesort/mergesort.why /usr/share/doc/why-2.29/examples/mlw/misc /usr/share/doc/why-2.29/examples/mlw/misc/arith.mlw /usr/share/doc/why-2.29/examples/mlw/misc/fib.mlw /usr/share/doc/why-2.29/examples/mlw/misc/flag.mlw /usr/share/doc/why-2.29/examples/mlw/misc/flag_ax.mlw /usr/share/doc/why-2.29/examples/mlw/misc/gcd.mlw /usr/share/doc/why-2.29/examples/mlw/misc/loop0.mlw /usr/share/doc/why-2.29/examples/mlw/misc/mac_carthy.mlw /usr/share/doc/why-2.29/examples/mlw/misc/matrix.why /usr/share/doc/why-2.29/examples/mlw/misc/matrix_mult.why /usr/share/doc/why-2.29/examples/mlw/misc/max.mlw /usr/share/doc/why-2.29/examples/mlw/misc/mix_max.mlw /usr/share/doc/why-2.29/examples/mlw/misc/peano.mlw /usr/share/doc/why-2.29/examples/mlw/misc/power.mlw /usr/share/doc/why-2.29/examples/mlw/misc/search.mlw /usr/share/doc/why-2.29/examples/mlw/misc/sqrt_dicho.mlw /usr/share/doc/why-2.29/examples/mlw/misc/sum.mlw /usr/share/doc/why-2.29/examples/mlw/misc/swap0.mlw /usr/share/doc/why-2.29/examples/mlw/queens /usr/share/doc/why-2.29/examples/mlw/queens/queens.why /usr/share/doc/why-2.29/examples/mlw/quicksort /usr/share/doc/why-2.29/examples/mlw/quicksort/partition.mlw /usr/share/doc/why-2.29/examples/mlw/quicksort/quicksort.mlw /usr/share/doc/why-2.29/examples/mlw/quicksort2 /usr/share/doc/why-2.29/examples/mlw/quicksort2/quicksort2.mlw /usr/share/doc/why-2.29/examples/mlw/selectionsort /usr/share/doc/why-2.29/examples/mlw/selectionsort/selection.mlw /usr/share/doc/why-2.29/examples/mlw/sqrt /usr/share/doc/why-2.29/examples/mlw/sqrt/simple.mlw /usr/share/doc/why-2.29/examples/mlw/sqrt/sqrt.mlw /usr/share/doc/why-2.29/krakatoa.pdf /usr/share/doc/why-2.29/why-manual.ps /usr/share/man/man1/why.1.gz
Generated by rpm2html 1.8.1
Fabrice Bellet, Mon May 20 07:38:10 2013