NAME
why - A multi-language multi-prover verification tool
SYNOPSIS
why [ options ] files
DESCRIPTION
why 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.
AUTHORS
Jean-Christophe Filliatre <filliatr@lri.fr>
SEE ALSO
Why web site: http://why.lri.fr/
March, 2002 why(1)