why-2.41-6.fc31.x86_64.rpm


Advertisement

Description

why - Software verification platform

Property Value
Distribution Fedora 31
Repository Fedora x86_64
Package filename why-2.41-6.fc31.x86_64.rpm
Package name why
Package version 2.41
Package release 6.fc31
Package architecture x86_64
Package type rpm
Homepage http://why.lri.fr/
License LGPLv2 with exceptions
Maintainer -
Download size 2.37 MB
Installed size 6.89 MB
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, Z3, 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).

Alternatives

Package Version Architecture Repository
why-2.41-8.fc31.x86_64.rpm 2.41 x86_64 Fedora Updates
why-2.41-6.fc31.x86_64.rpm 2.41 x86_64 Fedora Updates Testing
why - - -

Requires

Name Value
emacs-filesystem -
gappalib-coq -
hicolor-icon-theme -
libc.so.6(GLIBC_2.28)(64bit) -
libdl.so.2()(64bit) -
libdl.so.2(GLIBC_2.2.5)(64bit) -
libgmp.so.10()(64bit) -
libm.so.6()(64bit) -
libm.so.6(GLIBC_2.2.5)(64bit) -
libm.so.6(GLIBC_2.29)(64bit) -
rtld(GNU_HASH) -

Provides

Name Value
why = 2.41-6.fc31
why(x86-64) = 2.41-6.fc31

Download

Type URL
Mirror download-ib01.fedoraproject.org
Binary Package why-2.41-6.fc31.x86_64.rpm
Source Package why-2.41-6.fc31.src.rpm

Install Howto

Install why rpm package:

# dnf install why

Files

Path
/usr/bin/krakatoa
/usr/lib/.build-id/
/usr/lib/.build-id/ea/c3a446ddff3fb534d01f81511e7ba753f69e70
/usr/lib64/why/
/usr/lib64/why/coq/Jessie_memory_model.vo
/usr/lib64/why/java_api/
/usr/lib64/why/java_api/java/
/usr/lib64/why/java_api/java/io/BufferedWriter.java
/usr/lib64/why/java_api/java/io/File.java
/usr/lib64/why/java_api/java/io/FileDescriptor.java
/usr/lib64/why/java_api/java/io/FileNotFoundException.java
/usr/lib64/why/java_api/java/io/FileReader.java
/usr/lib64/why/java_api/java/io/FilterOutputStream.java
/usr/lib64/why/java_api/java/io/IOException.java
/usr/lib64/why/java_api/java/io/InputStream.java
/usr/lib64/why/java_api/java/io/InputStreamReader.java
/usr/lib64/why/java_api/java/io/ObjectStreamClass.java
/usr/lib64/why/java_api/java/io/OutputStream.java
/usr/lib64/why/java_api/java/io/OutputStreamWriter.java
/usr/lib64/why/java_api/java/io/PrintStream.java
/usr/lib64/why/java_api/java/io/Reader.java
/usr/lib64/why/java_api/java/io/Serializable.java
/usr/lib64/why/java_api/java/io/StreamTokenizer.java
/usr/lib64/why/java_api/java/lang/ArrayStoreException.java
/usr/lib64/why/java_api/java/lang/CharSequence.java
/usr/lib64/why/java_api/java/lang/Character.java
/usr/lib64/why/java_api/java/lang/Class.java
/usr/lib64/why/java_api/java/lang/Cloneable.java
/usr/lib64/why/java_api/java/lang/Comparable.java
/usr/lib64/why/java_api/java/lang/Double.java
/usr/lib64/why/java_api/java/lang/Exception.java
/usr/lib64/why/java_api/java/lang/IllegalArgumentException.java
/usr/lib64/why/java_api/java/lang/Integer.java
/usr/lib64/why/java_api/java/lang/Long.java
/usr/lib64/why/java_api/java/lang/Math.java
/usr/lib64/why/java_api/java/lang/Number.java
/usr/lib64/why/java_api/java/lang/NumberFormatException.java
/usr/lib64/why/java_api/java/lang/Object.java
/usr/lib64/why/java_api/java/lang/RuntimeException.java
/usr/lib64/why/java_api/java/lang/String.java
/usr/lib64/why/java_api/java/lang/StringBuffer.java
/usr/lib64/why/java_api/java/lang/System.java
/usr/lib64/why/java_api/java/lang/Throwable.java
/usr/lib64/why/java_api/java/util/AbstractMap.java
/usr/lib64/why/java_api/java/util/Collection.java
/usr/lib64/why/java_api/java/util/HashMap.java
/usr/lib64/why/java_api/java/util/HashMapIntegerInteger.java
/usr/lib64/why/java_api/java/util/HashMapIntegerLong.java
/usr/lib64/why/java_api/java/util/Iterator.java
/usr/lib64/why/java_api/java/util/Locale.java
/usr/lib64/why/java_api/java/util/Map.java
/usr/lib64/why/java_api/java/util/Set.java
/usr/lib64/why/javacard_api/
/usr/lib64/why/javacard_api/com/
/usr/lib64/why/javacard_api/com/sun/
/usr/lib64/why/javacard_api/com/sun/javacard/
/usr/lib64/why/javacard_api/com/sun/javacard/impl/Constants.java
/usr/lib64/why/javacard_api/com/sun/javacard/impl/NativeMethods.java
/usr/lib64/why/javacard_api/com/sun/javacard/impl/PackedBoolean.java
/usr/lib64/why/javacard_api/com/sun/javacard/impl/PrivAccess.java
/usr/lib64/why/javacard_api/java/
/usr/lib64/why/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java
/usr/lib64/why/javacard_api/java/lang/Exception.java
/usr/lib64/why/javacard_api/java/lang/IndexOutOfBoundsException.java
/usr/lib64/why/javacard_api/java/lang/Object.java
/usr/lib64/why/javacard_api/java/lang/RuntimeException.java
/usr/lib64/why/javacard_api/java/lang/Throwable.java
/usr/lib64/why/javacard_api/javacard/
/usr/lib64/why/javacard_api/javacard/framework/AID.java
/usr/lib64/why/javacard_api/javacard/framework/APDU.java
/usr/lib64/why/javacard_api/javacard/framework/APDUException.java
/usr/lib64/why/javacard_api/javacard/framework/Applet.java
/usr/lib64/why/javacard_api/javacard/framework/CardException.java
/usr/lib64/why/javacard_api/javacard/framework/CardRuntimeException.java
/usr/lib64/why/javacard_api/javacard/framework/Dispatcher.java
/usr/lib64/why/javacard_api/javacard/framework/ISO7816.java
/usr/lib64/why/javacard_api/javacard/framework/ISOException.java
/usr/lib64/why/javacard_api/javacard/framework/JCSystem.java
/usr/lib64/why/javacard_api/javacard/framework/OwnerPIN.java
/usr/lib64/why/javacard_api/javacard/framework/PIN.java
/usr/lib64/why/javacard_api/javacard/framework/PINException.java
/usr/lib64/why/javacard_api/javacard/framework/Shareable.java
/usr/lib64/why/javacard_api/javacard/framework/SystemException.java
/usr/lib64/why/javacard_api/javacard/framework/TransactionException.java
/usr/lib64/why/javacard_api/javacard/framework/UserException.java
/usr/lib64/why/javacard_api/javacard/framework/Util.java
/usr/lib64/why/javacard_api/javacard/security/CryptoException.java
/usr/lib64/why/javacard_api/javacard/security/DESKey.java
/usr/lib64/why/javacard_api/javacard/security/DSAKey.java
/usr/lib64/why/javacard_api/javacard/security/DSAPrivateKey.java
/usr/lib64/why/javacard_api/javacard/security/DSAPublicKey.java
/usr/lib64/why/javacard_api/javacard/security/Key.java
/usr/lib64/why/javacard_api/javacard/security/KeyBuilder.java
/usr/lib64/why/javacard_api/javacard/security/KeyPair.java
/usr/lib64/why/javacard_api/javacard/security/MessageDigest.java
/usr/lib64/why/javacard_api/javacard/security/PrivateKey.java
/usr/lib64/why/javacard_api/javacard/security/PublicKey.java
/usr/lib64/why/javacard_api/javacard/security/RSAPrivateCrtKey.java
/usr/lib64/why/javacard_api/javacard/security/RSAPrivateKey.java
/usr/lib64/why/javacard_api/javacard/security/RSAPublicKey.java
/usr/lib64/why/javacard_api/javacard/security/RandomData.java
/usr/lib64/why/javacard_api/javacard/security/SecretKey.java
/usr/lib64/why/javacard_api/javacard/security/Signature.java
/usr/lib64/why/javacard_api/javacardx/
/usr/lib64/why/javacard_api/javacardx/crypto/Cipher.java
/usr/lib64/why/why3/coq.drv
/usr/lib64/why/why3/jessie_why3.mlw
/usr/lib64/why/why3/jessie_why3theories.why
/usr/lib64/why/why3/why3.conf
/usr/share/doc/why/CHANGES
/usr/share/doc/why/README
/usr/share/doc/why/README.why
/usr/share/doc/why/README.why-coq.Fedora
/usr/share/doc/why/Version
/usr/share/doc/why/krakatoa.pdf
/usr/share/icons/hicolor/128x128/apps/why.png
/usr/share/icons/hicolor/22x22/apps/why.png
/usr/share/icons/hicolor/24x24/apps/why.png
/usr/share/icons/hicolor/256x256/apps/why.png
/usr/share/icons/hicolor/32x32/apps/why.png
/usr/share/icons/hicolor/48x48/apps/why.png
/usr/share/icons/hicolor/512x512/apps/why.png
/usr/share/icons/hicolor/64x64/apps/why.png
/usr/share/icons/hicolor/96x96/apps/why.png
/usr/share/licenses/why/COPYING
/usr/share/licenses/why/LICENSE

Changelog

2019-09-23 - Jerry James <loganjerry@gmail.com> - 2.41-6
- Rebuild for frama-c 19.1
2019-09-06 - Jerry James <loganjerry@gmail.com> - 2.41-5
- Rebuild for ocaml-zarith 1.9
2019-08-02 - Jerry James <loganjerry@gmail.com> - 2.41-4
- Rebuild for frama-c 19.0
2019-07-27 - Fedora Release Engineering <releng@fedoraproject.org> - 2.41-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
2019-06-05 - Jerry James <loganjerry@gmail.com> - 2.41-3
- Rebuild for coq 8.9.1, why3 1.2.0, and frama-c 18.0
2019-02-03 - Fedora Release Engineering <releng@fedoraproject.org> - 2.41-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
2019-01-26 - Jerry James <loganjerry@gmail.com> - 2.41-1
- New upstream release
- All patches have been upstreamed; drop them all
2018-07-14 - Fedora Release Engineering <releng@fedoraproject.org> - 2.40-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
2018-02-12 - Jerry James <loganjerry@gmail.com> - 2.40-1
- New upstream release
- Add -num patch to fix incomplete num to zarith conversion
2018-02-09 - Fedora Release Engineering <releng@fedoraproject.org> - 2.39-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild

See Also

Package Description
why-all-2.41-6.fc31.x86_64.rpm Complete Why software verification platform suite
why-jessie-2.41-6.fc31.x86_64.rpm Interface between why and frama-c
why-pvs-support-2.41-6.fc31.x86_64.rpm Complete Why software verification platform suite
why3-1.2.0-5.fc31.x86_64.rpm Software verification platform
why3-all-1.2.0-5.fc31.x86_64.rpm Complete Why3 software verification platform suite
why3-emacs-1.2.0-5.fc31.noarch.rpm Emacs support file for why3 files
why3-examples-1.2.0-5.fc31.noarch.rpm Example inputs
why3-xemacs-1.2.0-5.fc31.noarch.rpm XEmacs support file for why3 files
whysynth-dssi-20120903-9.fc31.x86_64.rpm DSSI software synthesizer plugin
wicd-kde-0.3.1-16.fc31.x86_64.rpm A Wicd client built on the KDE Development Platform
wide-dhcpv6-20080615-13.1.fc31.9.x86_64.rpm DHCP Client and Server for IPv6
widelands-0-0.72.build20.fc31.x86_64.rpm Open source realtime-strategy game
wifi-radar-2.0.s10-11.fc31.noarch.rpm A utility for managing WiFi profiles
wiggle-1.1-4.fc31.x86_64.rpm A tool for applying patches with conflicts
wiiuse-0.15.4-3.fc31.i686.rpm The wiiuse library is used to access and control multiple Nintendo Wiimotes
Advertisement
Advertisement