why and ergo
Before i put in a RTP, is there someone here willing to package
why and ergo? [Assuming they're not packaged yet ..]
http://why.lri.fr/
http://ergo.lri.fr/
Why is a software verification tool.
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, Ergo, Yices, CVC Lite and haRVey.
Why is developed by Jean-Christophe Filliâtre
Ergo is a nice theorem prover which uses Why syntax.
AFAIK both Why and Ergo are pure Ocaml code. Both build
easily on my Ubuntu box, they work, and they're awesome.
My Felix system now interfaces to Why, and allows you to
actually PROVE semantic properties of programs, so these
packages would become 'Recommends' for the Felix package.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
Reply to: