Ubuntu Manpage: Why3 - software verification platform

NAME

       Why3 - software verification platform

SYNOPSIS

       why3 [general options] <command> [command options] [command arguments]

DESCRIPTION

       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.

GENERAL OPTIONS

       -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

COMMANDS

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 subcommand detect forces Why3 to detect again the available provers and to
replace them in the configuration file.

If a supported prover is installed under a name that is not automatically
recognized by why3 config, the subcommand 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.

AUTHOR