Ubuntu
why package

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

View changes file

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.