Ubuntu
why package

why 2.29+dfsg-4 source package in Ubuntu

Changelog

why (2.29+dfsg-4) unstable; urgency=low

  * Rebuild with OCaml 3.12.1.
 -- Ubuntu Archive Auto-Sync <email address hidden>   Thu,  10 Nov 2011 16:42:27 +0000

Upload details

Uploaded by:
Ubuntu Archive Auto-Sync
Uploaded to:
Precise
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.29+dfsg.orig.tar.gz 2.6 MiB e0b78694c40770ea5632bf086f34446bd02f807d89f9f93c3f0563630d898a73
why_2.29+dfsg-4.debian.tar.gz 9.1 KiB 09381e71a23d250a5e131b1c33a566078a1cb9c0f9209334ef846bbfee7b60d0
why_2.29+dfsg-4.dsc 1.9 KiB 8503357475d0132bd351ee229c20fcc09f47bb3a7076e025fa097689c6b6e527

Available diffs

View changes file

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.