1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
.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://www.lri.fr/~filliatr/why/
|
