1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Source: why
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Samuel Mimram <smimram@debian.org>, Mehdi Dogguy <dogguy@pps.jussieu.fr>
Build-Depends: debhelper (>= 5), autotools-dev, ocaml-nox (>= 3.10), ocaml-best-compilers, camlp4, liblablgtk2-ocaml-dev, coq (>= 8.1.pl2+dfsg-3), libfloat-coq (>= 1:8.1-1.0-4), ocamlweb, libocamlgraph-ocaml-dev, dpatch
Standards-Version: 3.7.3
Vcs-Browser: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/why/trunk/
Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/why/trunk
Package: why
Architecture: any
Depends: ${shlibs:Depends}
Suggests: coq
Description: A 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, Ergo, Yices, CVC Lite and haRVey.
|
