Package: why3 (1.2.0-1)

[ Source: why3  ]

Programverifikationsplatform

Why3 er en platform for deduktiv programverifikation. Den tilbyder et rigt sprog for specifikation og programmering, kaldt WhyML, og afhænger af eksterne læresætningsbevisere, både automatiserede og interaktive, til at fjerne verifikationsbetingelser. Why3 har et standardbibliotek med logiske teorier (heltal og reel aritmetik, booleske operationer (tabeller, køer, hashtabeller etc.). En bruger kan skrive WhyML-programmer direkte og hente korrekt-efter-konstruktion OCaml-programmer via en automatiseret udtrækningsmekanisme. WhyML bruges også som et mellemliggende sprog for verifikation af C-, Java-, eller Ada-programmer.

Why3 er en fuldstændig ny implementering af den tidligere Why-platform. Blandt de nye funktioner er: utallige udvidelser for inddatasproget, en ny arkitektur for kald af eksterne bevisere, og en veldesignet API, der giver mulighed for at bruge Why3 som et programbibliotek. En vigtig del er lagt på modulopbygning og typeparametrisering, hvilket giver slutbrugeren en mulighed for nemt at genbruge Why3-formaliseringer eller tilføje understøttelse for en ny ekstern beviser hvis ønsket.

Tags: Interface Toolkit: GTK, Ncurses TUI

Other Packages Related to why3

• dep: libatk1.0-0 (>= 1.12.4)

  Værktøjssættet til ATK-tilgængelighed

• dep: libc6 (>= 2.28)

  GNU C-bibliotek: Delte biblioteker
  also a virtual package provided by libc6-udeb

• dep: libcairo-gobject2 (>= 1.10.0)

  Biblioteket for Cairo 2D-vektorgrafik - GObject-bibliotek

• dep: libcairo2 (>= 1.2.4)

  Cairo 2D - vektorgrafikbibliotek

• dep: libgdk-pixbuf2.0-0 (>= 2.22.0)

  GDK Pixbuf-bibliotek

• dep: libglib2.0-0 (>= 2.35.9)

  GLib-bibliotek for C-rutiner

• dep: libgtk-3-0 (>= 3.9.10)

  Grafisk brugergrænsefladebibliotek til GTK+

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

  delte bibliotekter for GTK+-kontrollen til fremhævelse af syntaks

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

  Layout og optegning af internationaliseret tekst

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

  Layout og optegning af internationaliseret tekst

• dep: ocaml-base-nox-4.05.0

  virtual package provided by ocaml-base-nox

• dep: tex-common (>= 6)

  Fælles infrastruktur for bygning og installation af TeX

• dep: zlib1g (>= 1:1.1.4)

  Komprimeringsbibliotek - kørselstid

• rec: cvc3

  Package not available

  or cvc4

  Automatiseret læresætningsbeviser for SMT-problemer

  or why3-coq

  Coq-understøttelse for why3-verifikationsplatformen

  or spass

  Package not available

  or z3

  Læresætningsbeviser fra Microsoft Research

  or alt-ergo (>= 2.0.0)

  Automatisk teorem-bevisfører dedikeret til programverifikation

• sug: why3-examples

  Eksempler for why3-verifikationsplatformen

Download why3

Download for all available architectures

Architecture	Package Size	Installed Size	Files
i386	19,485.2 kB	110,237.0 kB	[list of files]