1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
Source: why
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Samuel Mimram <smimram@debian.org>,
Mehdi Dogguy <mehdi@debian.org>
Build-Depends:
debhelper (>= 7.0.50~),
autotools-dev,
autoconf,
dh-ocaml (>= 0.9~),
ocaml-nox (>= 3.11.1-3~),
ocaml-best-compilers,
camlp4,
liblablgtk2-ocaml-dev (>= 2.12.0-3~),
coq (>= 8.3~),
libfloat-coq,
libocamlgraph-ocaml-dev (>= 1.4~),
frama-c-base (>= 20111001+nitrogen+dfsg-1~),
libapron-ocaml-dev (>= 0.9.10-4~),
camlidl
Standards-Version: 3.9.3
Homepage: http://why.lri.fr/
Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/why.git
Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/why.git
Package: why
Architecture: any
Depends:
${shlibs:Depends},
${ocaml:Depends},
${misc:Depends},
frama-c-base (= ${F:FramaCVersion}),
make
Suggests: libwhy-coq (= ${binary:Version})
Recommends: alt-ergo
Description: 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.
Package: why-examples
Architecture: all
Depends:
${misc:Depends},
libwhy-coq,
why
Section: doc
Description: 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.
Package: libwhy-coq
Architecture: all
Depends:
${misc:Depends},
coq-${F:CoqABI}
Replaces:
why (<< 2.18.dfsg-1)
Section: libdevel
Description: 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.
|
