Query: why
OS: debian
Section: 1
Format: Original Unix Latex Style Formatted with HTML and a Horizontal Scroll Bar
why(1) General Commands Manual why(1)NAMEwhy - A multi-language multi-prover verification toolSYNOPSISwhy [ options ] filesDESCRIPTIONwhy 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 <filliatr@lri.fr>SEE ALSOWhy web site: http://why.lri.fr/ March, 2002 why(1)