why-2.38-1.fc26.i686.rpm


Advertisement

Description

why - Software verification platform

Property Value
Distribution Fedora 26
Repository Fedora i386
Package name why
Package version 2.38
Package release 1.fc26
Package architecture i686
Package type rpm
Installed size 4.69 MB
Download size 2.02 MB
Official Mirror archives.fedoraproject.org
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.38-2.fc26.i686.rpm 2.38 i686 Fedora Updates
why-2.38-2.fc26.x86_64.rpm 2.38 x86_64 Fedora Updates
why-2.38-1.fc26.x86_64.rpm 2.38 x86_64 Fedora
why - - -

Requires

Name Value
emacs-filesystem -
gappalib-coq -
hicolor-icon-theme -
libc.so.6(GLIBC_2.15) -
libdl.so.2 -
libdl.so.2(GLIBC_2.0) -
libdl.so.2(GLIBC_2.1) -
libm.so.6 -
libm.so.6(GLIBC_2.0) -
libm.so.6(GLIBC_2.1) -
rtld(GNU_HASH) -

Provides

Name Value
why = 2.38-1.fc26
why(x86-32) = 2.38-1.fc26
why-coq = 2.38-1.fc26

Obsoletes

Name Value
why-coq < 2.36-1

Download

Type URL
Binary Package why-2.38-1.fc26.i686.rpm
Source Package why-2.38-1.fc26.src.rpm

Install Howto

Install the why rpm package:

# dnf install why

Files

Path
/usr/bin/krakatoa
/usr/lib/why/
/usr/lib/why/coq/Jessie_memory_model.vo
/usr/lib/why/java_api/
/usr/lib/why/java_api/java/
/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/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/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/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/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/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/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/Cipher.java
/usr/lib/why/why3/coq.drv
/usr/lib/why/why3/jessie_why3.mlw
/usr/lib/why/why3/jessie_why3theories.why
/usr/lib/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

2017-03-24 - Jerry James <loganjerry@gmail.com> - 2.38-1
- New upstream release
2017-02-11 - Fedora Release Engineering <releng@fedoraproject.org> - 2.36-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
2017-01-12 - Jerry James <loganjerry@gmail.com> - 2.36-1
- New upstream release
2016-11-30 - Jerry James <loganjerry@gmail.com> - 2.35-23
- Rebuild for gappalib-coq 1.3.2
2016-11-06 - Richard W.M. Jones <rjones@redhat.com> - 2.35-21
- Rebuild for OCaml 4.04.0.
- Modify configure script to allow building with OCaml 4.04.
- Modify configure script to use octMPQ library (part of Apron).
2016-10-28 - Jerry James <loganjerry@gmail.com> - 2.35-20
- Rebuild for coq 8.5pl3
- Remove obsolete scriptlets
2016-09-29 - Jerry James <loganjerry@gmail.com> - 2.35-19
- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
2016-09-02 - Jerry James <loganjerry@gmail.com> - 2.35-18
- Rebuild for why3 0.87.2
2016-07-22 - Jerry James <loganjerry@gmail.com> - 2.35-17
- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
2016-07-13 - Jerry James <loganjerry@gmail.com> - 2.35-16
- Rebuild for coq 8.5pl2

See Also

Package Description
why-all-2.38-1.fc26.i686.rpm Complete Why software verification platform suite
why-jessie-2.38-1.fc26.i686.rpm Interface between why and frama-c
why-pvs-support-2.38-1.fc26.i686.rpm Complete Why software verification platform suite
why3-0.87.3-3.fc26.i686.rpm Software verification platform
why3-all-0.87.3-3.fc26.i686.rpm Complete Why3 software verification platform suite
why3-emacs-0.87.3-3.fc26.noarch.rpm Emacs support file for why3 files
why3-examples-0.87.3-3.fc26.noarch.rpm Example inputs
why3-xemacs-0.87.3-3.fc26.noarch.rpm XEmacs support file for why3 files
whysynth-dssi-20120903-2.fc26.i686.rpm DSSI software synthesizer plugin
wicd-1.7.4-2.fc26.i686.rpm Wireless and wired network connection manager
wicd-common-1.7.4-2.fc26.noarch.rpm Wicd common files
wicd-curses-1.7.4-2.fc26.noarch.rpm Curses client for wicd
wicd-gtk-1.7.4-2.fc26.noarch.rpm GTK+ client for wicd
wicd-kde-0.3.1-10.fc26.i686.rpm A Wicd client built on the KDE Development Platform
wide-dhcpv6-20080615-13.1.fc26.3.i686.rpm DHCP Client and Server for IPv6
Advertisement
Advertisement