why3 0.88.3-1ubuntu2 source package in Ubuntu
Changelog
why3 (0.88.3-1ubuntu2) bionic; urgency=medium * Drop the why3+cvc4 test, since cvc4 is only available on x86 and there's no way to make autopkgtests per-architecture. -- Steve Langasek <email address hidden> Thu, 22 Mar 2018 23:21:56 -0700
Upload details
- Uploaded by:
- Steve Langasek
- 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.3.orig.tar.gz | 4.0 MiB | 3e6afd141800dce4d722794378e3eb8a9a05a06f8e51d520ff72159a3c6e3552 |
why3_0.88.3-1ubuntu2.debian.tar.xz | 13.0 KiB | 857b5f2649dfc4918f3518a5b05d3c0d18b1e4464f82df1364022d439a27d755 |
why3_0.88.3-1ubuntu2.dsc | 2.7 KiB | 75c345415abae0c4eb77710f44aa24c23b8e29de44ea1641c877182042644c2a |
Available diffs
- diff from 0.88.3-1ubuntu1 to 0.88.3-1ubuntu2 (476 bytes)
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.