Ubuntu
why package

why 2.30+dfsg-1 source package in Ubuntu

Changelog

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

 -- Mehdi Dogguy <email address hidden>  Mon, 02 Jan 2012 15:39:47 +0100

Upload details

Uploaded by:
Debian OCaml Maintainers
Uploaded to:
Sid
Original maintainer:
Debian OCaml Maintainers
Architectures:
any all
Section:
math
Urgency:
Low Urgency

See full publishing history Publishing

Series Pocket Published Component Section

Downloads

File Size SHA-256 Checksum
why_2.30+dfsg-1.dsc 1.9 KiB 876c38ef2aa8815c958946c0981b89b0ca4879db4e210fa44b5f95e8bc339823
why_2.30+dfsg.orig.tar.gz 3.1 MiB 51c91ead51875b0336d352eecd6b306a8f2c96414d59ec7f23b9f711b079cb90
why_2.30+dfsg-1.debian.tar.gz 10.5 KiB 743df22dbde89c2abc4169526d0f1fe3cf15fb15fdc46898a3d94ce6fae71a50

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: Software verification tool

 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.

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.