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.
Patching upstream sources
This package uses dpatch to manage all modifications to the upstream
source. Changes are stored in the source package as diffs in
debian/patches and applied during the build.
To get the fully patched source after unpacking the source package, cd
to the root level of the source package and run:
Removing a patch is as sim