|
Distribution |
Debian unstable |
Abteilung |
math |
Quelle |
why |
Version |
2.25+dfsg-1 |
Maintainer |
Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
|
Beschreibung |
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.
|
Abhängig von | libatk1.0-0 (>= 1.29.3), libc6 (>= 2.7), libcairo2 (>= 1.2.4), libfontconfig1 (>= 2.8.0), libfreetype6 (>= 2.2.1), libglib2.0-0 (>= 2.16.0), libgmp3c2, libgtk2.0-0 (>= 2.12.0), libmpfr1ldbl, libpango1.0-0 (>= 1.14.0), ocaml-base-nox-3.11.2 | Recommends | alt-ergo | Vorgeschlagen | libwhy-coq (= 2.25+dfsg-1) |
Offizielle Seiten |
Paket
Entwicklerinformationen
Bugs (Binärpaket)
Bugs (Quellpaket) |
Download |
amd64 |
|
|
|