why-examples binary package in Ubuntu Precise armel
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.
.
This package contains examples of programs verified using Why.
Publishing history
Date | Status | Target | Component | Section | Priority | Phased updates | Version | ||
---|---|---|---|---|---|---|---|---|---|
2012-01-17 16:38:19 UTC | Published | Ubuntu Precise armel | release | universe | doc | Optional | 2.30+dfsg-3 | ||
|
|||||||||
2012-01-17 18:04:43 UTC | Superseded | Ubuntu Precise armel | release | universe | doc | Optional | 2.30+dfsg-1 | ||
|
|||||||||
2012-01-08 14:34:24 UTC | Superseded | Ubuntu Precise armel | release | universe | doc | Optional | 2.29+dfsg-4build1 | ||
|
|||||||||
2011-11-19 20:04:07 UTC | Superseded | Ubuntu Precise armel | release | universe | doc | Optional | 2.29+dfsg-4 | ||
|
|||||||||
2011-11-12 21:05:05 UTC | Superseded | Ubuntu Precise armel | release | universe | doc | Optional | 2.29+dfsg-3 | ||
|