deb_control_files:
- conffiles
- control
- md5sums
- postinst
- postrm
- preinst
- prerm
deb_fields:
Architecture: amd64
Depends: libc6 (>= 2.35), libcairo2 (>= 1.2.4), libgdk-pixbuf-2.0-0 (>= 2.22.0),
libglib2.0-0 (>= 2.35.9), libgtk-3-0 (>= 3.11.5), libgtksourceview-3.0-1 (>= 2.91.4),
libpango-1.0-0 (>= 1.14.0), zlib1g (>= 1:1.1.4), libcairo2-ocaml-gl0g4, liblablgtk3-ocaml-0um05,
liblablgtksourceview3-ocaml-3azu2, ocaml-base-4.13.1, tex-common (>= 6.13)
Description: |-
Software verification platform
Why3 is a platform for deductive program verification. It provides a
rich language for specification and programming, called WhyML, and
relies on external theorem provers, both automated and interactive,
to discharge verification conditions. Why3 comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data
structures (arrays, queues, hash tables, etc.). A user can write
WhyML programs directly and get correct-by-construction OCaml
programs through an automated extraction mechanism. WhyML is also
used as an intermediate language for the verification of C, Java, or
Ada programs.
.
Why3 is a complete reimplementation of the former Why platform. Among
the new features are: numerous extensions to the input language, a
new architecture for calling external provers, and a well-designed
API, allowing to use Why3 as a software library. An important
emphasis is put on modularity and genericity, giving the end user a
possibility to easily reuse Why3 formalizations or to add support for
a new external prover if wanted.
Homepage: http://why3.lri.fr/
Installed-Size: '47319'
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Package: why3
Priority: optional
Recommends: cvc4 (<< 1.9) | spass | z3 (<< 4.11.1) | alt-ergo (>= 2.0.0)
Section: math
Source: why3 (1.5.1-1)
Suggests: why3-examples
Version: 1.5.1-1+b2
srcpkg_name: why3
srcpkg_version: 1.5.1-1