Ubuntu
why package

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 Pocket 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

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.