why_2.30+dfsg-5+b1_i386.deb


Advertisement

Description

why - Software verification tool

Property Value
Distribution Debian 7 (Wheezy)
Repository Debian Main i386
Package name why
Package version 2.30+dfsg
Package release 5+b1
Package architecture i386
Package type deb
Installed size 20.02 KB
Download size 7.13 MB
Official Mirror ftp.br.debian.org
Why aims at being a verification conditions generator (VCG) back-end
for other verification tools. It provides a powerful input language
including higher-order functions, polymorphism, references, arrays and
exceptions. It generates proof obligations for many systems: the proof
assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

Alternatives

Package Version Architecture Repository
why_2.30+dfsg-5+b1_amd64.deb 2.30+dfsg amd64 Debian Main
why - - -

Requires

Name Value
frama-c-base = 20111001+nitrogen+dfsg-4
libatk1.0-0 >= 1.12.4
libc6 >= 2.7
libcairo2 >= 1.2.4
libfontconfig1 >= 2.9.0
libfreetype6 >= 2.2.1
libgdk-pixbuf2.0-0 >= 2.22.0
libglib2.0-0 >= 2.24.0
libgmp10 -
libgtk2.0-0 >= 2.24.0
libmpfr4 >= 3.1.0
libpango1.0-0 >= 1.14.0
make -
ocaml-base-nox-3.12.1 -

Download

Type URL
Binary Package why_2.30+dfsg-5+b1_i386.deb
Source Package why

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install why deb package:
    # sudo apt-get install why

Files

Path
/usr/bin/gwhy
/usr/bin/gwhy-bin
/usr/bin/jessie
/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/frama-c/plugins/Jessie.cma
/usr/lib/frama-c/plugins/Jessie.cmi
/usr/lib/frama-c/plugins/Jessie.cmxs
/usr/share/doc/why/README
/usr/share/doc/why/README.source
/usr/share/doc/why/changelog.Debian.gz
/usr/share/doc/why/changelog.gz
/usr/share/doc/why/copyright
/usr/share/man/man1/caduceus.1.gz
/usr/share/man/man1/gwhy-bin.1.gz
/usr/share/man/man1/gwhy.1.gz
/usr/share/man/man1/jessie.1.gz
/usr/share/man/man1/krakatoa.1.gz
/usr/share/man/man1/rv_merge.1.gz
/usr/share/man/man1/simplify2why.1.gz
/usr/share/man/man1/tool-stat.1.gz
/usr/share/man/man1/why-config.1.gz
/usr/share/man/man1/why-cpulimit.1.gz
/usr/share/man/man1/why-dp.1.gz
/usr/share/man/man1/why-obfuscator.1.gz
/usr/share/man/man1/why-stat.1.gz
/usr/share/man/man1/why.1.gz
/usr/share/man/man1/why2html.1.gz
/usr/share/why/coq/Why.v
/usr/share/why/coq/Why.vo
/usr/share/why/coq/WhyArrays.v
/usr/share/why/coq/WhyArrays.vo
/usr/share/why/coq/WhyBool.v
/usr/share/why/coq/WhyBool.vo
/usr/share/why/coq/WhyCM.v
/usr/share/why/coq/WhyCM.vo
/usr/share/why/coq/WhyCoqCompat.v
/usr/share/why/coq/WhyCoqCompat.vo
/usr/share/why/coq/WhyExn.v
/usr/share/why/coq/WhyExn.vo
/usr/share/why/coq/WhyFloatsStrictLegacy.v
/usr/share/why/coq/WhyFloatsStrictLegacy.vo
/usr/share/why/coq/WhyInt.v
/usr/share/why/coq/WhyInt.vo
/usr/share/why/coq/WhyLemmas.v
/usr/share/why/coq/WhyLemmas.vo
/usr/share/why/coq/WhyPermut.v
/usr/share/why/coq/WhyPermut.vo
/usr/share/why/coq/WhyPrelude.v
/usr/share/why/coq/WhyPrelude.vo
/usr/share/why/coq/WhyReal.v
/usr/share/why/coq/WhyReal.vo
/usr/share/why/coq/WhySorted.v
/usr/share/why/coq/WhySorted.vo
/usr/share/why/coq/WhyTactics.v
/usr/share/why/coq/WhyTactics.vo
/usr/share/why/coq/WhyTuples.v
/usr/share/why/coq/WhyTuples.vo
/usr/share/why/coq/jessie_why.v
/usr/share/why/coq/jessie_why.vo
/usr/share/why/emacs/why.el
/usr/share/why/images/accept-bw.png
/usr/share/why/images/accept32.png
/usr/share/why/images/bug-bw.png
/usr/share/why/images/bug32.png
/usr/share/why/images/clock-bw.png
/usr/share/why/images/clock32.png
/usr/share/why/images/delete-bw.png
/usr/share/why/images/delete32.png
/usr/share/why/images/help-bw.png
/usr/share/why/images/help32.png
/usr/share/why/images/logo-why-small.png
/usr/share/why/images/pause-bw.png
/usr/share/why/images/pause32.png
/usr/share/why/images/play-bw.png
/usr/share/why/images/play32.png
/usr/share/why/images/stop-bw.png
/usr/share/why/images/stop32.png
/usr/share/why/images/why-logo-1.png
/usr/share/why/java_api/java/io/BufferedWriter.java
/usr/share/why/java_api/java/io/File.java
/usr/share/why/java_api/java/io/FileDescriptor.java
/usr/share/why/java_api/java/io/FileNotFoundException.java
/usr/share/why/java_api/java/io/FileReader.java
/usr/share/why/java_api/java/io/FilterOutputStream.java
/usr/share/why/java_api/java/io/IOException.java
/usr/share/why/java_api/java/io/InputStream.java
/usr/share/why/java_api/java/io/InputStreamReader.java
/usr/share/why/java_api/java/io/ObjectStreamClass.java
/usr/share/why/java_api/java/io/OutputStream.java
/usr/share/why/java_api/java/io/OutputStreamWriter.java
/usr/share/why/java_api/java/io/PrintStream.java
/usr/share/why/java_api/java/io/Reader.java
/usr/share/why/java_api/java/io/Serializable.java
/usr/share/why/java_api/java/io/StreamTokenizer.java
/usr/share/why/java_api/java/lang/ArrayStoreException.java
/usr/share/why/java_api/java/lang/CharSequence.java
/usr/share/why/java_api/java/lang/Character.java
/usr/share/why/java_api/java/lang/Class.java
/usr/share/why/java_api/java/lang/Cloneable.java
/usr/share/why/java_api/java/lang/Comparable.java
/usr/share/why/java_api/java/lang/Double.java
/usr/share/why/java_api/java/lang/Exception.java
/usr/share/why/java_api/java/lang/IllegalArgumentException.java
/usr/share/why/java_api/java/lang/Integer.java
/usr/share/why/java_api/java/lang/Long.java
/usr/share/why/java_api/java/lang/Math.java
/usr/share/why/java_api/java/lang/Number.java
/usr/share/why/java_api/java/lang/NumberFormatException.java
/usr/share/why/java_api/java/lang/Object.java
/usr/share/why/java_api/java/lang/RuntimeException.java
/usr/share/why/java_api/java/lang/String.java
/usr/share/why/java_api/java/lang/StringBuffer.java
/usr/share/why/java_api/java/lang/System.java
/usr/share/why/java_api/java/lang/Throwable.java
/usr/share/why/java_api/java/util/AbstractMap.java
/usr/share/why/java_api/java/util/Collection.java
/usr/share/why/java_api/java/util/HashMap.java
/usr/share/why/java_api/java/util/HashMapIntegerInteger.java
/usr/share/why/java_api/java/util/HashMapIntegerLong.java
/usr/share/why/java_api/java/util/Iterator.java
/usr/share/why/java_api/java/util/Locale.java
/usr/share/why/java_api/java/util/Map.java
/usr/share/why/java_api/java/util/Set.java
/usr/share/why/javacard_api/com/sun/javacard/impl/Constants.java
/usr/share/why/javacard_api/com/sun/javacard/impl/NativeMethods.java
/usr/share/why/javacard_api/com/sun/javacard/impl/PackedBoolean.java
/usr/share/why/javacard_api/com/sun/javacard/impl/PrivAccess.java
/usr/share/why/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java
/usr/share/why/javacard_api/java/lang/Exception.java
/usr/share/why/javacard_api/java/lang/IndexOutOfBoundsException.java
/usr/share/why/javacard_api/java/lang/Object.java
/usr/share/why/javacard_api/java/lang/RuntimeException.java
/usr/share/why/javacard_api/java/lang/Throwable.java
/usr/share/why/javacard_api/javacard/framework/AID.java
/usr/share/why/javacard_api/javacard/framework/APDU.java
/usr/share/why/javacard_api/javacard/framework/APDUException.java
/usr/share/why/javacard_api/javacard/framework/Applet.java
/usr/share/why/javacard_api/javacard/framework/CardException.java
/usr/share/why/javacard_api/javacard/framework/CardRuntimeException.java
/usr/share/why/javacard_api/javacard/framework/Dispatcher.java
/usr/share/why/javacard_api/javacard/framework/ISO7816.java
/usr/share/why/javacard_api/javacard/framework/ISOException.java
/usr/share/why/javacard_api/javacard/framework/JCSystem.java
/usr/share/why/javacard_api/javacard/framework/OwnerPIN.java
/usr/share/why/javacard_api/javacard/framework/PIN.java
/usr/share/why/javacard_api/javacard/framework/PINException.java
/usr/share/why/javacard_api/javacard/framework/Shareable.java
/usr/share/why/javacard_api/javacard/framework/SystemException.java
/usr/share/why/javacard_api/javacard/framework/TransactionException.java
/usr/share/why/javacard_api/javacard/framework/UserException.java
/usr/share/why/javacard_api/javacard/framework/Util.java
/usr/share/why/javacard_api/javacard/security/CryptoException.java
/usr/share/why/javacard_api/javacard/security/DESKey.java
/usr/share/why/javacard_api/javacard/security/DSAKey.java
/usr/share/why/javacard_api/javacard/security/DSAPrivateKey.java
/usr/share/why/javacard_api/javacard/security/DSAPublicKey.java
/usr/share/why/javacard_api/javacard/security/Key.java
/usr/share/why/javacard_api/javacard/security/KeyBuilder.java
/usr/share/why/javacard_api/javacard/security/KeyPair.java
/usr/share/why/javacard_api/javacard/security/MessageDigest.java
/usr/share/why/javacard_api/javacard/security/PrivateKey.java
/usr/share/why/javacard_api/javacard/security/PublicKey.java
/usr/share/why/javacard_api/javacard/security/RSAPrivateCrtKey.java
/usr/share/why/javacard_api/javacard/security/RSAPrivateKey.java
/usr/share/why/javacard_api/javacard/security/RSAPublicKey.java
/usr/share/why/javacard_api/javacard/security/RandomData.java
/usr/share/why/javacard_api/javacard/security/SecretKey.java
/usr/share/why/javacard_api/javacard/security/Signature.java
/usr/share/why/javacard_api/javacardx/crypto/Cipher.java
/usr/share/why/why/arrays.why
/usr/share/why/why/bool.why
/usr/share/why/why/divisions.why
/usr/share/why/why/floats_common.why
/usr/share/why/why/floats_full.why
/usr/share/why/why/floats_multi_rounding.why
/usr/share/why/why/floats_strict.why
/usr/share/why/why/integer.why
/usr/share/why/why/jessie.why
/usr/share/why/why/jessie_bitvectors.why
/usr/share/why/why/mix.why
/usr/share/why/why/mybag.why
/usr/share/why/why/prelude.why
/usr/share/why/why/real.why
/usr/share/why/why3/jessie3.mlw
/usr/share/why/why3/jessie3.why

Changelog

2012-05-16 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-5) unstable; urgency=low
* Update 0001-Why-2.29-do-support-Coq-8.3.patch
- Mark Coq 8.3pl4 as compatible.
* Bump Standards-Version to 3.9.3, no changes required.
2012-04-06 - St├ęphane Glondu <glondu@debian.org>
why (2.30+dfsg-4) unstable; urgency=high
* Team upload
* Recompile with coq 8.3pl4 (no changes)
2012-01-16 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-3) unstable; urgency=high
* Fix 0002-Mark-alt-ergo-0.93-as-compatible.patch
- Adapt version_regexp because "alt-ergo -version" changed.
* Fix 0004-Default-to-why2-for-jessie-atp.patch
- default to "gui" instead of "why2".
* Add 0007-Replace-caduceus-invocation-by-Frama-C.patch
- Caduceus is gone. We use Frama-C instead.
- Adding Frama-C to Why's dependencies.
* Setting urgency to "high" to fix those issues.
2012-01-12 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-2) unstable; urgency=low
* Rebuilt with latest coq-float 1:8.3pl1-1 (no source changes).
2012-01-02 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-1) unstable; urgency=low
* New upstream release.
* Update patches:
- Rebase and update existing patches
- add 0004-Default-to-why2-for-jessie-atp.patch
- add 0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
* Add (back) Build-Depends on coq-float.
* Bump build requirement for frama-c to 20111001+nitrogen+dfsg-1~.
* Bump Standards-Version to 3.9.2, no changes needed.
* Fix description-synopsis-starts-with-article in why's description.
* Fix copyright-refers-to-deprecated-bsd-license-file
* Fix spelling-error-in-binary
* Mark Coq 8.3pl3 as compatible with current Why
2011-11-03 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-4) unstable; urgency=low
* Rebuild with OCaml 3.12.1.
2011-04-25 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-3) unstable; urgency=low
* Remove last added patch. The problem was in Makefile.dynamic, shipped
by frama-c-base which lacks some include statements.
- remove 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
- Bump minimum version number for Frama-C to 20110201+carbon+dfsg-2~.
2011-04-25 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-2) unstable; urgency=low
* Fix FTBFS on armel.
- add 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
2011-04-24 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-1) unstable; urgency=low
* New upstream release.
- Remove old patches, which are not needed anymore.
- Remove build-depends on coq-float (upstream switched to Flocq which
is not packaged yet).
* Bump minimum version of Coq to 8.3
- and add 0001-Why-2.29-do-support-Coq-8.3.patch (upstream forgot to
mention to why-config that Coq 8.3 is "ok").
* Mark Alt-Ergo 0.93 as compatible
- add 0002-Mark-alt-ergo-0.93-as-compatible.patch
* Fix FTBFS due to non-exhaustive pattern matching
- add 0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
* Set 20110201+carbon+dfsg-1~ as minimum version number for Frama-C.
2011-03-11 - St├ęphane Glondu <glondu@debian.org>
why (2.26+dfsg-4) unstable; urgency=low
* Team upload
* Rebuild with coq 8.2.pl2+dfsg-2 (no changes)

See Also

Package Description
whysynth_20090403-1.2_i386.deb DSSI Soft Synth Interface
whyteboard_0.41.1-4_all.deb overlay painting and annotation application
wicd-cli_1.7.2.4-4_all.deb wired and wireless network manager - scriptable console client
wicd-curses_1.7.2.4-4_all.deb wired and wireless network manager - Curses client
wicd-daemon_1.7.2.4-4_all.deb wired and wireless network manager - daemon
wicd-gtk_1.7.2.4-4_all.deb wired and wireless network manager - GTK+ client
wicd-kde_0.3.0-2_i386.deb Wired and wireless network manager - plasmoid
wicd_1.7.2.4-4_all.deb wired and wireless network manager - metapackage
wide-dhcpv6-client_20080615-11.1_i386.deb DHCPv6 client for automatic IPv6 hosts configuration
wide-dhcpv6-relay_20080615-11.1_i386.deb DHCPv6 relay for automatic IPv6 hosts configuration
wide-dhcpv6-server_20080615-11.1_i386.deb DHCPv6 server for automatic IPv6 hosts configuration
widelands-data_17-3_all.deb fantasy real-time strategy game (data files)
widelands_17-3_i386.deb fantasy real-time strategy game
widemargin_1.0.11-4_all.deb bible reading and study application
wifi-radar_2.0.s08+dfsg-1.1_all.deb graphical utility for managing Wi-Fi profiles
Advertisement
Advertisement