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)