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 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
