Section: User Commands (1)Updated: March, 2002Local indexUp
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.