why 2.30+dfsg-3 source package in Ubuntu
Changelog
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. -- Mehdi Dogguy <email address hidden> Mon, 16 Jan 2012 18:19:38 +0100
Upload details
- Uploaded by:
- Debian OCaml Maintainers
- Uploaded to:
- Sid
- Original maintainer:
- Debian OCaml Maintainers
- Architectures:
- any all
- Section:
- math
- Urgency:
- Very Urgent
See full publishing history Publishing
Series | Published | Component | Section | |
---|---|---|---|---|
Precise | release | universe | math |
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
why_2.30+dfsg-3.dsc | 1.9 KiB | 1206ee64d95ad18771e74b7f962d0e849f2bd608e7b5152f59da8c56189b2446 |
why_2.30+dfsg.orig.tar.gz | 3.1 MiB | 51c91ead51875b0336d352eecd6b306a8f2c96414d59ec7f23b9f711b079cb90 |
why_2.30+dfsg-3.debian.tar.gz | 11.0 KiB | 8f2798db8f649764564edd5f9dfcdafb4e557e9cf7c8ce62cc70716818595870 |
Available diffs
- diff from 2.30+dfsg-1 to 2.30+dfsg-3 (2.0 KiB)
No changes file available.
Binary packages built by this source
- libwhy-coq: Why library for Coq
This package contains all useful logical definitions, lemmas with their
proofs and axioms used by Why. Users may need this package when proving
some proof obligations in Coq.
- why: No summary available for why in ubuntu quantal.
No description available for why in ubuntu quantal.
- why-examples: Examples of programs certified with Why
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.
.
This package contains examples of programs verified using Why.