why 2.34-4ubuntu1 source package in Ubuntu
Changelog
why (2.34-4ubuntu1) xenial; urgency=medium * Rebase on Debian, remaining change: + debian/tests/control: Disable frama-c+jessie+alt-ergo test, since we don't have a jessie plugin currently (until we get 'why3') why (2.34-4) unstable; urgency=medium [ Ralf Treinen ] * improve as-installed package tests [ Mehdi Dogguy ] * Fix FTBFS with OCaml 4.02.3 by: - not using Format.bprintf anymore - not turning warning 3 into an error * Port Why to ocamlgraph 1.8.6 -- Iain Lane <email address hidden> Wed, 04 Nov 2015 12:12:10 +0000
Upload details
- Uploaded by:
- Iain Lane
- Uploaded to:
- Xenial
- Original maintainer:
- Debian OCaml Maintainers
- Architectures:
- any all
- Section:
- math
- Urgency:
- Medium Urgency
See full publishing history Publishing
Series | Published | Component | Section |
---|
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
why_2.34.orig.tar.gz | 3.6 MiB | 76f3af8cf3857424852ca76eb87c99ff6089aadc3271da6b829ca84529f9c733 |
why_2.34-4ubuntu1.debian.tar.xz | 11.1 KiB | 2b55c3544c7ae93e9fd0bd52c0cba2688001907e33b12d22f901637ed3d8c68e |
why_2.34-4ubuntu1.dsc | 2.3 KiB | 0868a2ccf4a3c555e0388125d9184bb14331fe42c7c5cdb3dcc8c1f21b224c9e |
Available diffs
- diff from 2.34-2ubuntu3 to 2.34-4ubuntu1 (2.9 KiB)
Binary packages built by this source
- libwhy-coq: No summary available for libwhy-coq in ubuntu xenial.
No description available for libwhy-coq in ubuntu xenial.
- 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-dbgsym: debug symbols for package 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.
- 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.