Provided by: why3_0.88.3-3ubuntu1_amd64
Why3 - software verification platform
why3 [general options] <command> [command options] [command arguments]
This manual page summarizes basic information about the why3 command. Please refer to the Reference Manual for complete information. Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called whyml, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write whyml programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. whyml is also used as an intermediate language for the verification of C, Java, or Ada programs.
-C <file> read configuration from <file> --config same as -C --extra-config <file> read additional configuration from <file> -L <dir> add <dir> to the library search path --library same as -L --debug <flag> set a debug flag --debug-all set all debug flags that do not change Why3 behaviour --list-debug-flags list known debug flags --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 --print-libdir print location of binary components (plugins, etc) --print-datadir print location of non-binary data (theories, modules, etc) --version print version information -h print this list of options --help same as -h
config Creates a why3 configuration file ~/.why3.conf, containing in particular information about available provers and plugins. If this file exists already, config will only reset unset variables to default value, but will not try to detect provers. The command option --detect-provers can be used to force Why3 to detect again the available provers and to replace them in the configuration file. The command option --detect-plugins does the same for plugins. If a supported prover is installed under a name that is not automatically recognized by why3 config, the command option --add-prover adds a specified binary to the configuration. For example, an Alt-Ergo executable /home/me/bin/alt-ergo- trunk can be added as follows: why3 config --add-prover alt-ergo /home/me/bin/alt-ergo-trunk doc produces HTML pages from Why3 source code. execute symbolically executes programs written in the WhyML language extract extracts OCaml code from programs written in the WhyML language ide launches the graphical user interface of the why3 platform. There are no specific command options. However, at least one command argument must be given. More precisely, the first argument must be the directory of the session. If the directory does not exist, it is created. The other arguments should be existing files that are going to be added to the session. For convenience, if there is only one argument, it can be an existing file and in this case the session directory is obtained by removing the extension from the file name. prove launches why3 in batch mode on a an input file realize produces skeleton files for proof assistants replay executes the proofs stored in a Why3 session file, as produced by the IDE. session wc produces statistics about Why3 and WhyML source codes.
The information on this manpage was extracted from the complete Why3 reference manual.
On a debian system, the full documentation for why3 is distributed in PDF and HTML format in the packages why3-doc-html and why3-doc-pdf. It is also available from the why3 homepage <http://why3.lri.fr>.