Ubuntu
why3 package

why3 1.2.1-3 source package in Ubuntu

Changelog

why3 (1.2.1-3) unstable; urgency=medium

  [ Stéphane Glondu ]
  * Team upload
  * Fix FTBFS with menhir 20200123 (Closes: #951052)

  [ Ralf Treinen ]
  * drop cvc3 from Recommends and debian/tests as the cvc3 package has
    been removed from sid.

 -- Stéphane Glondu <email address hidden>  Mon, 10 Feb 2020 13:57:51 +0100

Upload details

Uploaded by:
Debian OCaml Maintainers
Uploaded to:
Sid
Original maintainer:
Debian OCaml Maintainers
Architectures:
any all
Section:
misc
Urgency:
Medium Urgency

See full publishing history Publishing

Series Pocket Published Component Section

Downloads

File Size SHA-256 Checksum
why3_1.2.1-3.dsc 2.4 KiB 080279720fb443a6c2a2876ac9ca07c9fb8f02b7df3e410ecaa50ced239df028
why3_1.2.1.orig.tar.gz 5.7 MiB 8798ffbe1c455d7ab39692c1d09f15e0267196cfb37f41c6e8055ca9239f8f04
why3_1.2.1-3.debian.tar.xz 17.1 KiB f8d110d0a40268603b40b5b821d581a7ec4d1a785a2e1c4acb02c62d8c84c73f

No changes file available.

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.

libwhy3-ocaml-dev-dbgsym: debug symbols for libwhy3-ocaml-dev
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.

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.