Paket: why3 (1.8.0-3)

[ Källkod: why3  ]

Experimentellt paket

Varning: Paketet är från den experimentella utgåvan. Det innebär att det med stor sannolikhet är instabilt eller innehåller fel, och kanske till och med kan orsaka dataförluster. Se till att läsa ändringsloggen och annan dokumentation innan du använder det.

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.

Märken: Interface Toolkit: GTK, Ncurses TUI

Andra paket besläktade med why3

• dep: libc6 (>= 2.38)

  GNU C-bibliotek: Delade bibliotek
  också ett virtuellt paket som tillhandahålls av libc6-udeb

• dep: libcairo2 (>= 1.2.4)

  Cairo 2D vector graphics library

• dep: libcairo2-ocaml-7ye75

  Paketet inte tillgängligt

• dep: libgdk-pixbuf-2.0-0 (>= 2.22.0)

  GDK Pixbuf library

• dep: libglib2.0-0t64 (>= 2.36.0)

  GLib library of C routines

• dep: libgmp10 (>= 2:6.3.0+dfsg)

  Multiprecision arithmetic library

• dep: libgtk-3-0t64 (>= 3.11.5)

  GTK graphical user interface library

• dep: libgtksourceview-3.0-1 (>= 2.91.4)

  shared libraries for the GTK+ syntax highlighting widget

• dep: liblablgtk3-ocaml-636l7

  Paketet inte tillgängligt

• dep: liblablgtksourceview3-ocaml-gu9y1

  Paketet inte tillgängligt

• dep: libpango-1.0-0 (>= 1.14.0)

  Layout and rendering of internationalized text

• dep: libstdlib-ocaml-ke4j9

  Paketet inte tillgängligt

• dep: tex-common (>= 6.13)

  common infrastructure for building and installing TeX

• dep: zlib1g (>= 1:1.1.4)

  Kompressionsbibliotek - körtidspaket

• rec: cvc4 (<< 1.9)

  automated theorem prover for SMT problems

  eller cvc5 (<< 1.3)

  automated theorem prover for SMT problems

  eller spass

  automated theorem prover for first-order logic with equality

  eller z3 (<< 4.14)

  theorem prover from Microsoft Research

• sug: why3-examples

  Examples for the why3 verification platform

Hämta why3

Hämtningar för alla tillgängliga arkitekturer

Arkitektur	Paketstorlek	Installerad storlek	Filer
s390x	12.138,5 kbyte	48.627,0 kbyte	[filförteckning]