.TH why 1 "March, 2002"

.SH NAME
why \- A multi-language multi-prover verification tool


.SH SYNOPSIS
.B why
[
.B options
]
.B files


.SH DESCRIPTION

.B 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).

.SH OPTIONS

.TP
.B \-h
Help. Will give you the full list of command line options.


.SH AUTHORS
.I Jean-Christophe Filliatre <filliatr@lri.fr>


.SH SEE ALSO

.I
Why web site: http://why.lri.fr/