why 2.34-1 source package in Ubuntu

Changelog

why (2.34-1) unstable; urgency=low


  * New upstream release.
  * Drop deprecated patches:
    - deprecated-or
    - hashtbl
    - frama-c-versions
  * Bump build-dependency on frama-c to version 20140301+neon+dfsg.
  * Fix debian/tests/frama-c+jessie+alt-ergo:
    - run why-config when there is no ${HOME}/.whyrc
    - drop the specification of cpp-4.7 as this is no longer needed, and
      the dependency of that test on cpp-4.7
  
 -- Ralf Treinen <email address hidden>  Tue, 29 Apr 2014 20:56:03 +0200

Upload details

Uploaded by:
Debian OCaml Maintainers on 2014-04-30
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.34-1.dsc 2.3 KiB dbf3aeed4d7aa7fe8a19c73e2ce607455ffbd8a17b25daeec9154880798a970d
why_2.34.orig.tar.gz 3.6 MiB 76f3af8cf3857424852ca76eb87c99ff6089aadc3271da6b829ca84529f9c733
why_2.34-1.debian.tar.xz 10.2 KiB 896570e910ae37b76b376099f70dc91abd42e7745e46dba0d479303e8ed0c1f2

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: 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.