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
Component:
main
Architectures:
any all
Section:
math
Urgency:
Low Urgency

See full publishing history Publishing

Series Pocket Published Component Section

Downloads

File Size MD5 Checksum
why_2.34-1.dsc 2.3 KiB f4e005f41bb3f4f368af748b3aee26a9
why_2.34.orig.tar.gz 3.6 MiB 1e729c4ecb41892531563d34208d3e52
why_2.34-1.debian.tar.xz 10.2 KiB f01e225f1a3a2c3ce65d842bf0f28230

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.