| Paketname | why |
| Beschreibung | A software verification tool |
| Archiv/Repository | Offizielles Debian Archiv squeeze (main) |
| Version | 2.26+dfsg-2+squeeze1 |
| Sektion | math |
| Priorität | optional |
| Installierte Größe | 21712 Byte |
| Hängt ab von | libatk1.0-0 (>= 1.29.3), libc6 (>= 2.7), libcairo2 (>= 1.2.4), libfontconfig1 (>= 2.8.0), libfreetyp |
| Empfohlene Pakete | alt-ergo |
| Paketbetreuer | Debian OCaml Maintainers |
| Quelle | |
| Paketgröße | 7654940 Byte |
| Prüfsumme MD5 | e8cc0425d8e70a06e9dd88abc86cbad7 |
| Prüfsumme SHA1 | d6ec5bd780e74777ef8141c00cb6d52b7069a7d3 |
| Prüfsumme SHA256 | fe5c609644087498c5453ab216fb7103956b5b83bf131cc2120e17f3de4ef87b |
| Link zum Herunterladen | why_2.26+dfsg-2+squeeze1_i386.deb |
| Ausführliche Beschreibung | 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.
|