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.88.2 why3 User Commands