why3ml - Man Page

generate verification conditions from Why3ML programs


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


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.


-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 selected theories from the library.


Reduce the set of needed axioms which prove a goal, and output the resulting task.


Print selected theories.


Print namespaces of selected theories.


List known transformations.


List known printers.


List known provers.


List known input formats.


List known metas.


List known debug flags.


Stop after parsing (same as --debug parse_only).


Stop after type checking (same as --debug type_only).


Set all debug flags except parse_only and type_only.

--debug <flag>

Set a debug flag.


Print location of binary components (plugins, etc.).


Print location of non-binary data (theories, modules, etc.).


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).

1.3.3 why3