This chapter details the usage of each of the command-line tools provided by the Why3 environment. The main command is why3; it acts as an entry-point to all the features of Why3. It is invoked as such
why3 [general options...] <command> [specific options...]
The following commands are available:
All these commands are also available as standalone executable files, if needed.
The commands accept a common subset of command-line options. In
particular, option --help
displays the usage and options.
-L
.
-C
.
Why3 must be configured to access external provers. Typically, this is done by running the config command. This must be done each time a new prover is installed.
The provers that Why3 attempts to detect are described in the readable configuration file provers-detection-data.conf of the Why3 data directory (e.g. /usr/local/share/why3). Advanced users may try to modify this file to add support for detection of other provers. (In that case, please consider submitting a new prover configuration on the bug tracking system.)
The result of provers detection is stored in the user’s
configuration file (~/.why3.conf
or, in the case of local
installation, why3.conf
in Why3 sources top directory). This file
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, e.g. different
versions of the same prover, or with different options.
The config command also detects the plugins installed in the Why3 plugins directory (e.g. /usr/local/lib/why3/plugins). A plugin must register itself as a parser, a transformation or a printer, as explained in the corresponding section.
If the user’s configuration file is already present,
config will only reset unset variables to default value,
but will not try to detect provers.
The option --detect-provers
should be used to force
Why3 to detect again the available
provers and to replace them in the configuration file. The option
--detect-plugins
will do the same for plugins.
If a supported prover is installed under a name
that is not automatically recognized by why3config,
the option --add-prover
will add 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 alt-ergo-trunk /home/me/bin/alt-ergo-trunk
As the first argument, one should put a prover family
identification string. The list of known prover families
can be obtained by the option --list-prover-families
.
Why3 is primarily used to call provers on goals contained in an input file. By default, such a file must be written in WhyML language (extension .mlw). However, a dynamically loaded plugin can register a parser for some other format of logical problems, e.g. TPTP or SMT-LIB.
The prove command executes the following steps:
--format
option to choose
among the available parsers. why3 --list-formats
lists
the registered parsers.
WhyML modules are turned into
theories containing verification conditions as goals.
-G/--goal
and -T/--theory
. Option
-T/--theory
applies to the previous file appearing on the
command line. Option -G/--goal
applies to the previous theory
appearing on the command line. If no theories are selected in a file,
then every theory is considered as selected. If no goals are selected
in a theory, then every goal is considered as selected.
-a/--apply-transform
in their order of appearance on the
command line. why3 --list-transforms
lists the known
transformations; plugins can add more of them.
-D/--driver
option,
or the driver of the prover selected with the -P/--prover
option. why3 --list-provers
lists the known provers, i.e. the ones
that appear in the configuration file.
-P/--prover
is given, call the selected prover
on each generated task and print the results. If option
-D/--driver
is given, print each generated task using
the format specified in the selected driver.
The provers can give the following output:
That feature is presented in details in Section 5.3.7, that should be read first.
Counterexamples are also displayed by the why3 prove command when one selects a prover with the counterexamples alternative. The output is currently done in a JSON syntax (this may change in the future).
The basic usage of the GUI is described by the tutorial of Section 1.2. The command-line options are the common options detailed in introduction to this chapter, plus the specific option already described for the command prove in Section 5.2.2.
At least one anonymous argument must be specified on the command line. More precisely, the first anonymous 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 anonymous argument, it can be an existing file and in this case the session directory is obtained by removing the extension from the file name.
We describe the actions of the various menus and buttons of the interface.
Why3 stores in a session the way you achieve to prove goals that come from a file (.why), from weakest-precondition (.mlw) or by other means. A session stores which file you prove, by applying which transformations, by using which prover. A proof attempt records the complete name of a prover (name, version, optional attribute), the time limit and memory limit given, and the result of the prover. The result of the prover is the same as when you run the prove command. It contains the time taken and the state of the proof:
Additionally, a proof attempt can have the following attributes:
Generally, proof attempts are marked obsolete just after the start of the user interface. Indeed, when you load a session in order to modify it (not with why3session info for instance), Why3 rebuilds the goals to prove by using the information provided in the session. If you modify the original file (.mlw) or if the transformations have changed (new version of Why3), Why3 will detect that. Since the provers might answer differently on these new proof obligations, the corresponding proof attempts are marked obsolete.
The left toolbar that was present in former versions of Why3 is now replaced by a context menu activited by clicking the right mouse button, while cursor is on a given row of the proof session tree.
For automatic provers, this allows to see the file sent to the prover.
For interactive provers, this also allows to add or modify the corresponding proof script. The modifications are saved, and can be retrieved later even if the goal was modified.
Between the top-right zone containing source files and task, and the bottom-right zone containing various messages, a text input field allows the user to invoke commands using a textual interface (see Figure 1.1). The ’help’ command displays a basic list of available commands. All commands available in the menus are also available as a textual command. However the textual interface allows for much more possibilities, including the ability to invoke transformations with arguments.
The preferences dialog allows you to customize various settings. They are grouped together under several tabs.
Note that there are to different buttons to close that dialog. The “Close” button will make modifications of any of these settings effective only for the current run of the GUI. The “Save&Close” button will save the modified settings in Why3 configuration file, to make them permanent.
Why3 provides some support for extracting a potential counterexample from failing proof attempts, for provers that are able to produce a counter-model of the proof task. Why3 attempts to turn this counter-model into values for the free variables of the original Why3 input. Currently, this is supported for CVC4 prover version at least 1.5, and Z3 prover version at least 4.4.0.
The generation of counterexamples is fully integrated in Why3 IDE. The recommended usage is to first start a prover normally, as shown in Figure 5.1) and then click on the status icon for the corresponding proof attempt in the tree. Alternatively, one can use the key shortcut “G” or type get-ce in the command entry. The result can be seen on Figure 5.2: the same prover but with the alternative counterexamples is run. The resulting counterexample is displayed in two different ways. First, it is displayed in the Task tab of the top-right window, at the end of the text of the task, under the form of a list of pairs “variable = value”, ordered by the line number of the source code in which that variable takes that value. Second, it is displayed in the Counterexample tab of the bottom right window, this time interleaved with the code, as shown in Figure 5.2.
![]()
Figure 5.1: Failing execution of CVC4
![]()
Figure 5.2: Counterexamples display for CVC4
The counterexamples can contain values of various types.
To detail the display of map values, consider the following code with a trivially false postcondition:
use int.Int use ref.Ref use map.Map let ghost test_map (ghost x : ref (map int int)) : unit ensures { !x[0] <> !x[1] } = x := Map.set !x 0 3 |
Executing CVC4 with the “counterexamples” alternative on goal will trigger counterexamples:
use int.Int use ref.Ref use map.Map let ghost test_map (ghost x : ref (map int int)) : unit (* x = (1 => 3,others => 0) *) ensures { !x[0] <> !x[1] } (* x = (0 => 3,1 => 3,others => 0) *) = x := Map.set !x 0 3 (* x = (0 => 3,1 => 3,others => 0) *) |
The notation for map is to be understood with indices on left of the arrows and values on the right “(index => value)”. The meaning of the keyword others is the value for all indices that were not mentioned yet. This shows that setting the parameter x to a map that has value 3 for index 1 and zero for all other indices is a counterexample. We can check that this negates the Why3ensures clause.
The counterexamples are known not to work on the following non-exhaustive list (which is undergoing active development):
More information on the implementation of counterexamples in Why3 can be found in [7] and in [5]. For the producing counterexamples using the Why3 API, see Section 3.10.
The replay command is meant to execute the proofs stored in a Why3 session file, as produced by the IDE. Its main purpose is to play non-regression tests. For instance, examples/regtests.sh is a script that runs regression tests on all the examples.
The tool is invoked in a terminal or a script using
The session file why3session.xml stored in the given directory is loaded and all the proofs it contains are rerun. Then, all the differences between the information stored in the session file and the new run are shown.
Nothing is shown when there is no change in the results, whether the considered goal is proved or not. When all the proof are done, a summary of what is proved or not is displayed using a tree-shape pretty print, similar to the IDE tree view after doing “Collapse proved goals”. In other words, when a goal, a theory, or a file is fully proved, the subtree is not shown.
When some proof attempts stored in the session file are obsolete, the replay is run anyway, as with the replay button in the IDE. Then, the session file will be updated if both
In other cases, you can use the IDE to update the session, or use the
option --force
described below.
The exit code is 0 if no difference was detected, 1 if there was. Other exit codes mean some failure in running the replay.
Options are:
The smoke detector tries to detect if the context is self-contradicting and, thus, that anything can be proved in this context. The smoke detector can’t be run on an outdated session and does not modify the session. It has three possible configurations:
Goal G : forall x:int. q x -> (p1 x \/ p2 x)becomes
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))In other words, if the smoke detector is triggered, it means that the context of the goal G is self-contradicting.
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)In other words, the premises of goal G are pushed in the context, so that if the smoke detector is triggered, it means that the context of the goal G and its premises are self-contradicting. It should be clear that detecting smoke in that case does not necessarily means that there is a mistake: for example, this could occur in the WP of a program with an unfeasible path.
At the end of the replay, the name of the goals that triggered the smoke detector are printed:
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
Moreover Smoke detected (exit code 1) is printed at the end if the smoke detector has been triggered, or No smoke detected (exit code 0) otherwise.
The session command makes it possible to extract information from proof sessions on the command line, or even modify them to some extent. The invocation of this program is done under the form
why3 session <subcommand> [options] <session directories>
The available subcommands are as follows:
The first three commands do not modify the sessions, whereas the last modify them.
The command why3 session info reports various informations about the session, depending on the following specific options.
provers
and --edited-files
by the character number 0
instead of end of line \n
. That allows you to safely use
(even if the filename contains space or carriage return) the result
with other commands. For example you can count the number of proof
line in all the coq edited files in a session with:
why3 session info --edited-files vstte12_bfs --print0 | xargs -0 coqwcor you can add all the edited files in your favorite repository with:
why3 session info --edited-files --print0 vstte12_bfs.mlw | \ xargs -0 git add
The proof statistics given by option --stats
are as follows:
For example, here are the session statistics produced on the “hello proof” example of Section 1.
== Number of root goals ==
total: 3 proved: 2
== Number of sub goals ==
total: 2 proved: 1
== Goals not proved ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G2
+-- transformation split_goal_right
+-- goal G2.0
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G1: Alt-Ergo 0.99.1
+-- goal G2
+-- transformation split_goal_right
+-- goal G2.1: Alt-Ergo 0.99.1
+-- goal G3: Alt-Ergo 0.99.1
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
Alt-Ergo 0.99.1 : 3 0.00 0.00 0.00
Command latex produces a summary of the replay under the form of a tabular environment in LaTeX, one tabular for each theory, one per file.
The specific options are
file.theory.goal
. The
file produced is named accordingly,
e.g. file.theory.goal.tex
. This option can be given several
times to produce several tables in one run. When this option is
given at least once, the default behavior that is to produce one
table per theory is disabled.
The generated LaTeX files contain some macros that must be defined externally. Various definitions can be given to them to customize the output.
\usepackage{xcolor} \usepackage{colortbl} \usepackage{rotating} \newcommand{\provername}[1]{\cellcolor{yellow!25} \begin{sideways}\textbf{#1}~~\end{sideways}} \newcommand{\explanation}[1]{\cellcolor{yellow!13}lemma \texttt{#1}} \newcommand{\transformation}[1]{\cellcolor{yellow!13}transformation \texttt{#1}} \newcommand{\subgoal}[2]{\cellcolor{yellow!13}subgoal #2} \newcommand{\valid}[1]{\cellcolor{green!13}#1} \newcommand{\unknown}[1]{\cellcolor{red!20}#1} \newcommand{\invalid}[1]{\cellcolor{red!50}#1} \newcommand{\timeout}[1]{\cellcolor{red!20}(#1)} \newcommand{\outofmemory}[1]{\cellcolor{red!20}(#1)} \newcommand{\noresult}{\multicolumn{1}{>{\columncolor[gray]{0.8}}c|}{~}} \newcommand{\failure}{\cellcolor{red!20}failure} \newcommand{\highfailure}{\cellcolor{red!50}FAILURE}
Figure 5.3: Sample macros for the LaTeX command
Figure 5.4: LaTeX table produced for the HelloProof example (style 1)
Figure 5.5: LaTeX table produced for the HelloProof example (style 2)
Figure 5.3 suggests some definitions for these macros, while Figures 5.4 and 5.5 show the tables obtained from the HelloProof example of Section 1, respectively with style 1 and 2.
This command produces a summary of the proof session in HTML syntax. There are two styles of output: ‘table’ and ‘simpletree’. The default is ‘table’.
The file generated is named why3session.html and is written in the session directory by default (see option -o to override this default).
Why3 Proof Results for Project "hello_proof"
Theory "hello_proof.HelloProof": not fully verified
Obligations Alt-Ergo 0.99.1 Coq 8.7.1 G1 0.00 --- G2 0.00 --- split_goal_right G2.0 0.00 0.29 G2.1 0.00 --- G3 0.00 ---
Figure 5.6: HTML table produced for the HelloProof example
The style ‘table’ outputs the contents of the session as a table, similar to the LaTeX output above. Figure 5.6 is the HTML table produced for the ‘HelloProof’ example, as typically shown in a Web browser. The gray cells filled with --- just mean that the prover was not run on the corresponding goal. Green background means the result was “Valid”, other cases are in orange background. The red background for a goal means that the goal was not proved.
The style ‘simpletree’ displays the contents of the session under the
form of tree, similar to the tree view in the IDE. It uses only basic
HTML tags such as <ul>
and <li>
.
Specific options for this command are as follows.
coqdoc
command to display Coq proof
scripts. This is equivalent to --add_pp .v "coqdoc
--no-index --html -o %o %i" .htmlThe command why3 session update permits to modify the session contents, depending on the following specific options.
This tool can produce HTML pages from Why3 source code. Why3 code for theories or modules is output in preformatted HTML code. Comments are interpreted in three different ways.
Additionally, all the Why3 identifiers are typeset with links so that one can navigate through the HTML documentation, going from some identifier use to its definition.
-o
.
Some constructs are interpreted:
A CSS file style.css
suitable for rendering is generated in the
same directory as output files. This CSS style can be modified manually,
since regenerating the HTML documentation will not overwrite an existing
style.css
file.
Why3 can symbolically execute programs written using the WhyML language (extension .mlw). See also Section 7.1.
Why3 can extract programs written using the WhyML language (extension .mlw) to OCaml. See also Section 7.2.
Why3 can produce skeleton files for proof assistants that, once filled, realize the given theories. See also Section 8.2.
Why3 can give some token statistics about WhyML source files.