Package: why (2.30+dfsg-5)

[ Source: why  ]

Software verification tool

Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

Tags: Software Development: Testing and QA, Implemented in: OCaml, Role: Program

Other Packages Related to why

• dep: frama-c-base (= 20111001+nitrogen+dfsg-4)

  Framework for C source code analysis (without gui)

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

  sada nástrojov prístupnosti ATK

• dep: libc6 (>= 2.7)

  knižnica Embedded GNU C - zdieľané knižnice
  also a virtual package provided by libc6-udeb

• dep: libcairo2 (>= 1.2.4)

  knižnica 2D vektorovej grafiky

• dep: libfontconfig1 (>= 2.9.0)

  všeobecná knižnica na konfiguráciu písiem - dynamické knižnice

• dep: libfreetype6 (>= 2.2.1)

  správa písiem FreeType 2 - zdieľané knižnice

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

  knižnica GDK Pixbuf

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

  knižnica glib funkcií jazyka C

• dep: libgmp10

  aritmetická knižnica s viacnásobnou presnosťou

• dep: libgtk2.0-0 (>= 2.24.0)

  knižnica grafického používateľského rozhrania GTK+

• dep: libmpfr4 (>= 3.1.0)

  výpočty s plávajúcou desatinnou čiarkou s viacnásobnou presnosťou

• dep: libpango1.0-0 (>= 1.14.0)

  rozloženie a vykreslenie internacionalizovaného textu

• dep: make

  nástroj na riadenie kompilácie

• dep: ocaml-base-nox-3.12.1

  virtual package provided by ocaml-base-nox

• rec: alt-ergo

  Automatic theorem prover dedicated to program verification

• sug: libwhy-coq (= 2.30+dfsg-5)

  Why library for Coq

Download why

Download for all available architectures

Architecture	Package Size	Installed Size	Files
sparc	7,918.8 kB	21,691.0 kB	[list of files]