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 Ubuntu Archiv lucid (universe)
Version2.23+dfsg-2
Sektionuniverse/doc
Prioritätoptional
Installierte Größe2160 Byte
Hängt ab vonlibwhy-coq, why
Empfohlene Pakete
PaketbetreuerUbuntu Developers
Quellewhy
Paketgröße184678 Byte
Prüfsumme MD57182085ecba19f5bdfc0814233737f40
Prüfsumme SHA1ddd0d2e8919c4e2050fb175bb3a679f5ca7c66c1
Prüfsumme SHA256a2792b208efbb2a60704f6ad3050e235cdfade39a44281312941634dbdd10a6e
Link zum Herunterladenwhy-examples_2.23+dfsg-2_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