why3ml man page

why3ml — generate verification conditions from Why3ML programs

Synopsis

why3ml [Options] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]

Description

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

Options

-T, --theory <theory>
Select theory in the input file or in the library.
-G, --goal <goal>
Select goal in the last selected theory.
-C, --config <file>
Read configuration from file.
-L, --library <dir>
Add dir to the library search path.
-P, --prover <prover>
Prove or print (with -o) the selected goals using prover.
-F, --format <format>
Select the input format (default: "why").
-t, --timelimit <sec>
Set the prover's time limit in seconds, where 0 means no limit (default: 10).
-m, --memlimit <MiB>
Set the prover's memory limit in megabytes (default: no limit).
-a, --apply-transform <transformation>
Apply a transformation to every task.
-M, --meta <metaname>=<string>
Add a string meta to every task.
-D, --driver <file>
Specify a prover's driver (conflicts with -P).
-o, --output <dir>
Print the selected goals to separate files in dir.
--realize
Realize selected theories from the library.
--bisect
Reduce the set of needed axioms which prove a goal, and output the resulting task.
--print-theory
Print selected theories.
--print-namespace
Print namespaces of selected theories.
--list-transforms
List known transformations.
--list-printers
List known printers.
--list-provers
List known provers.
--list-formats
List known input formats.
--list-metas
List known metas.
--list-debug-flags
List known debug flags.
--parse-only
Stop after parsing (same as --debug parse_only).
--type-only
Stop after type checking (same as --debug type_only).
--debug-all
Set all debug flags except parse_only and type_only.
--debug <flag>
Set a debug flag.
--print-libdir
Print location of binary components (plugins, etc.).
--print-datadir
Print location of non-binary data (theories, modules, etc.).
--version
Print version information.
-help, --help
Show a list of options.

See Also

why3(1), why3-cpulimit(1), why3bench(1), why3config(1), why3doc(1), why3ide(1), why3realize(1), why3replayer(1)

Referenced By

why3(1), why3bench(1), why3config(1), why3-cpulimit(1), why3doc(1), why3ide(1), why3realize(1), why3replayer(1).

0.87.2 why3 User Commands