NAMEwhy - A multi-language multi-prover verification tool
SYNOPSISwhy [ options ] files
DESCRIPTIONwhy is a verification tool. It takes annotated programs as input (in ML or C syntax) and outputs verification conditions for several proof assistants (Coq, PVS, HOL Light, Mizar) and decision procedures (haRVey, Simplify).
OPTIONS-h Help. Will give you the full list of command line options.
AUTHORSJean-Christophe Filliatre <email@example.com>
SEE ALSOWhy web site: //why.lri.fr/ March, 2002 WHY(1)