Provided by: why3_0.88.3-3ubuntu1_amd64 bug


       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>

              same as -C

       --extra-config <file> read additional configuration from <file>

       -L <dir>
              add <dir> to the library search path

              same as -L

       --debug <flag>
              set a debug flag

              set all debug flags that do not change Why3 behaviour

              list known debug flags

              list known transformations

              list known printers

              list known provers

              list known input formats

              list known metas

              print location of binary components (plugins, etc)

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

              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.

              symbolically executes programs written in the WhyML language

              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

              produces skeleton files for proof assistants

       replay executes the proofs stored in a Why3 session file, as produced by the IDE.


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