1why(1)                      General Commands Manual                     why(1)
2
3
4

NAME

6       why - A multi-language multi-prover verification tool
7
8
9

SYNOPSIS

11       why [ options ] files
12
13
14

DESCRIPTION

16       why  is  a verification tool.  It takes annotated programs as input (in
17       ML or C syntax) and outputs verification conditions for  several  proof
18       assistants  (Coq,  PVS, HOL Light, Mizar) and decision procedures (haR‐
19       Vey, Simplify).
20
21

OPTIONS

23       -h     Help. Will give you the full list of command line options.
24
25
26

AUTHORS

28       Jean-Christophe Filliatre <filliatr@lri.fr>
29
30
31

SEE ALSO

33       Why web site: http://why.lri.fr/
34
35
36
37
38                                  March, 2002                           why(1)