why3 0.88.2-1ubuntu1 source package in Ubuntu
Changelog
why3 (0.88.2-1ubuntu1) bionic; urgency=low * Merge from Debian unstable. Remaining changes: - Skip why3+z3 test on ppc64el/s390x, as it hangs indefinately. why3 (0.88.2-1) unstable; urgency=medium * New upstream version. * Standards-Version 4.1.2 (no change) * d/rules: - recreate in target configure the empty directories that are in the orig tarball. - invoke dh_missing with --fail-missing * fix why3.install, add missing files from usr/lib * Added build-dep-indep texlive-bibtex-extra * debhelper compat level 10 * New SMT solver cvc4: - add as an alternative Recommends - add autopkgtest test case -- Gianfranco Costamagna <email address hidden> Thu, 14 Dec 2017 08:40:43 +0100
Upload details
- Uploaded by:
- Gianfranco Costamagna
- Uploaded to:
- Bionic
- Original maintainer:
- Ubuntu Developers
- Architectures:
- any all
- Section:
- misc
- Urgency:
- Medium Urgency
See full publishing history Publishing
Series | Published | Component | Section |
---|
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
why3_0.88.2.orig.tar.gz | 4.3 MiB | 83f2c8887aa9717d5dcc03bde16b495a93819826f7a06277adbdf2f3be33d8f8 |
why3_0.88.2-1ubuntu1.debian.tar.xz | 12.9 KiB | a87be22136b68add9381d7e8aeb704310e688f3cdd58f4de2cd5dca821bb8a23 |
why3_0.88.2-1ubuntu1.dsc | 2.7 KiB | b3e4ccee265255690c118b09a1071e5a5ec9975431df0d5e3435dcbca5e2023b |
Available diffs
Binary packages built by this source
- libwhy3-ocaml-dev: OCaml librariries for why3 (dev)
This package contains the libraries of the why3 verification platform
for developing applications using why3.
- why3: 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.
- why3-coq: Coq support for the why3 verification platform
This package contains the compiled coq files that are necessary to
use the coq proof assistant together with the why3 deductive
verification platform, as well as the why3 tactic for coq.
- why3-coq-dbgsym: debug symbols for why3-coq
- why3-dbgsym: debug symbols for why3
- why3-doc-html: HTML Documentation of the why3 verification platform
This package contains the tutorial and reference manual of the
why3 verification platform in HTML format.
- why3-doc-pdf: PDF Documentation of the why3 verification platform
This package contains the tutorial and reference manual of the
why3 verification platform in PDF format.
- why3-examples: Examples for the why3 verification platform
This package contains examples, both of program verification tasks
and pure logical verification tasks, for the why3 software verification
platform.