1WHY3ML(1)                        User Commands                       WHY3ML(1)
2
3
4

NAME

6       why3ml - generate verification conditions from Why3ML programs
7

SYNOPSIS

9       why3ml [OPTIONS] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]
10

DESCRIPTION

12       This  tool is an additional layer on top of the Why3 library for gener‐
13       ating verification conditions from Why3ML  programs.   It  accepts  the
14       same  command  line options as why3, but also accepts files with exten‐
15       sion .mlw as input files containing Why3ML modules.  Modules are turned
16       into  theories  containing  verification  conditions as goals, and then
17       why3ml behaves exactly as why3 for the remainder of the process.   Note
18       that files with extension .mlw can also be loaded in why3ide.
19

OPTIONS

21       -T, --theory <theory>
22              Select theory in the input file or in the library.
23
24       -G, --goal <goal>
25              Select goal in the last selected theory.
26
27       -C, --config <file>
28              Read configuration from file.
29
30       -L, --library <dir>
31              Add dir to the library search path.
32
33       -P, --prover <prover>
34              Prove or print (with -o) the selected goals using prover.
35
36       -F, --format <format>
37              Select the input format (default: "why").
38
39       -t, --timelimit <sec>
40              Set  the  prover's time limit in seconds, where 0 means no limit
41              (default: 10).
42
43       -m, --memlimit <MiB>
44              Set the prover's memory limit in megabytes (default: no limit).
45
46       -a, --apply-transform <transformation>
47              Apply a transformation to every task.
48
49       -M, --meta <metaname>=<string>
50              Add a string meta to every task.
51
52       -D, --driver <file>
53              Specify a prover's driver (conflicts with -P).
54
55       -o, --output <dir>
56              Print the selected goals to separate files in dir.
57
58       --realize
59              Realize selected theories from the library.
60
61       --bisect
62              Reduce the set of needed axioms which prove a goal,  and  output
63              the resulting task.
64
65       --print-theory
66              Print selected theories.
67
68       --print-namespace
69              Print namespaces of selected theories.
70
71       --list-transforms
72              List known transformations.
73
74       --list-printers
75              List known printers.
76
77       --list-provers
78              List known provers.
79
80       --list-formats
81              List known input formats.
82
83       --list-metas
84              List known metas.
85
86       --list-debug-flags
87              List known debug flags.
88
89       --parse-only
90              Stop after parsing (same as --debug parse_only).
91
92       --type-only
93              Stop after type checking (same as --debug type_only).
94
95       --debug-all
96              Set all debug flags except parse_only and type_only.
97
98       --debug <flag>
99              Set a debug flag.
100
101       --print-libdir
102              Print location of binary components (plugins, etc.).
103
104       --print-datadir
105              Print location of non-binary data (theories, modules, etc.).
106
107       --version
108              Print version information.
109
110       -help, --help
111              Show a list of options.
112

SEE ALSO

114       why3(1),  why3-cpulimit(1),  why3bench(1),  why3config(1),  why3doc(1),
115       why3ide(1), why3realize(1), why3replayer(1)
116
117
118
119why3                                 1.3.1                           WHY3ML(1)
Impressum