DEBFIND Suche nach Debian-Paketen

Suchplatform für Softwarepakete und Archive Debian-basierter Linux-Distributionen

beta ! Diese website wird noch weiterentwickelt.

Liste aller Kategorien/Sektionen | Suchmaske | Haftungsausschluß

Paketbeschreibung


Paketnamewhy-examples
BeschreibungExamples of programs certified with Why
Archiv/RepositoryOffizielles Debian Archiv squeeze (main)
Version2.26+dfsg-2+squeeze1
Sektiondoc
Prioritätoptional
Installierte Größe2148 Byte
Hängt ab vonlibwhy-coq, why
Empfohlene Pakete
PaketbetreuerDebian OCaml Maintainers
Quellewhy
Paketgröße184102 Byte
Prüfsumme MD5bd3252cc0d3ff31950d444039b6fce76
Prüfsumme SHA1bbd3f70629f0de7fd7474ec545898b8564bfa1ce
Prüfsumme SHA2563429343a4d0edb7eb5fc718f932537fce7f2468e3504bf6d881d8cf7e980a41e
Link zum Herunterladenwhy-examples_2.26+dfsg-2+squeeze1_all.deb
Ausführliche BeschreibungWhy 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. . This package contains examples of programs verified using Why.

Impressum
Linux is a registered trademark of Linus Torvalds