Previous Up Next

Chapter 6  Reference Manuals for the Why3 Tools

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:

bench
produces benchmarks.
config
manages the user’s configuration, including the detection of installed provers.
doc
produces HTML versions of Why3 source codes.
execute
performs a symbolic execution of WhyML input files.
extract
generates an OCaml program corresponding to WhyML input files.
ide
provides a graphical interface to display goals and to run provers and transformations on them.
prove
reads Why3 and WhyML input files and calls provers, on the command-line.
realize
generates interactive proof skeletons for Why3 input files.
replay
replays the proofs stored in a session, for regression test purposes.
session
dumps various informations from a proof session, and possibly modifies the session.
wc
gives some token statistics about Why3 and WhyML source codes.

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 <dir>
adds <dir> in the load path, to search for theories.
--library <dir>
is the same as -L.
-C <file>
reads the configuration from the given file.
--config <file>
is the same as -C.
--extra-config <file>
reads additional configuration from the given file.
--list-debug-flags
lists known debug flags.
--debug-all
sets all debug flags (except flags which change the behavior).
--debug <flag>
sets a specific debug flag.
--help
displays the usage and the exact list of options for the given tool.

6.1  The config Command

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 /home/me/bin/alt-ergo-trunk

As the first argument, one should put a prover identification string. The list of known prover identifiers can be obtained by the option --list-prover-ids.

6.2  The prove Command

Why3 is primarily used to call provers on goals contained in an input file. By default, such a file must be written either in Why3 language (extension .why) or 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:

  1. Parse the command line and report errors if needed.
  2. Read the configuration file using the priority defined in Section 10.3.
  3. Load the plugins mentioned in the configuration. It will not stop if some plugin fails to load.
  4. Parse and typecheck the given files using the correct parser in order to obtain a set of Why3 theories for each file. It uses the filename extension or the --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.
  5. Extract the selected goals inside each of the selected theories into tasks. The goals and theories are selected using options -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.
  6. Apply the transformations requested with -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.
  7. Apply the driver selected with the -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.
  8. If option -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.

6.2.1  Prover Results

The provers can give the following output:

Valid
The goal is proved in the given context.
Unknown
The prover has stopped its search.
Timeout
The prover has reached the time limit.
Failure
An error has occurred.
Invalid
The prover knows the goal cannot be proved.

6.2.2  Additional Options

--get-ce
activates the generation of a potential counter-example when a proof does not succeed (experimental).
--extra-expl-prefix <s>
specifies s as an additional prefix for labels that denotes VC explanations. The option can be used several times to specify several prefixes.

6.3  The ide Command

The basic usage of the GUI is described by the tutorial of Section 1.2. There are no specific command-line options, apart from the common options detailed in introduction to this chapter. However 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.

6.3.1  Session

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:

Valid
The task is valid according to the prover. The goal is considered proved.
Invalid
The task is invalid.
Timeout
the prover exceeded the time limit.
OufOfMemory
The prover exceeded the memory limit.
Unknown
The prover cannot determine if the task is valid. Some additional information can be provided.
Failure
The prover reported a failure.
HighFailure
An error occurred while trying to call the prover, or the prover answer was not understood.

Additionally, a proof attempt can have the following attributes:

obsolete
The prover associated to that proof attempt has not been run on the current task, but on an earlier version of that task. You need to replay the proof attempt, i.e. run the prover with the current task of the proof attempt, in order to update the answer of the prover and remove this attribute.
archived
The proof attempt is not useful anymore; it is kept for history; no Why3 tools will select it by default. Section 5.6 shows an example of this usage.

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 (.why, .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.

6.3.2  Left toolbar actions

Context
presents the context in which the other tools below will apply. If “only unproved goals” is selected, no action will ever be applied to an already proved goal. If “all goals”, then actions are performed even if the goal is already proved. The second choice allows to compare provers on the same goal.
Strategies
section provides a set of actions that are performed on the selected goal(s):
Split
splits the current goal into subgoals if it is a conjunction of two or more goals. It corresponds to the split_goal_wp transformation.
Inline
inlines the definitions in the conclusion of the goal. It corresponds to the introduce_premises transformation follwoed by inline_goal.
Auto level 1
is a strategy that first applies a few provers on the goal with a short time limit, then splits the goal and tries again on the subgoals
Auto level 2
is a strategy more elaborate than level 1, that attempts to apply a few transformations that are typically useful. It also tries the provers with a larger time limit.
A more detailed description of strategies is given in Section 10.6, as well as a description on how to design strategies of your own.
Provers
provide a button for each detected prover. Clicking on such a button starts the corresponding prover on the selected goal(s).
Tools
section provides a set of specific action that are typically performed on the selected goal(s). :
Edit
starts an editor on the selected task.

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.

Replay
replays all the obsolete proofs.

If “only unproved goals” is selected, only formerly successful proofs are rerun. If “all goals”, then all obsolete proofs are rerun, successful or not.

Remove
removes a proof attempt or a transformation.
Clean
removes any unsuccessful proof attempt for which there is another successful proof attempt for the same goal
Interrupt
cancels all the proof attempts currently scheduled but not yet started.

6.3.3  Menus

Menu File
 
Add File
adds a file in the GUI. ]
Preferences
opens a window for modifying preferred configuration parameters, see details below.
Reload
reloads the input files from disk, and update the session state accordingly.
Save session
saves current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
Quit
exits the GUI.
Menu View
 
Expand All
expands all the rows of the tree view.
Collapse proved goals
closes all the rows of the tree view that are proved.
Menu Tools
A copy of the tools already available in the left toolbar, plus:
Mark as obsolete
marks all the proof as obsolete. This allows to replay every proof.
Non-splitting transformation
applies one of the available transformations, as listed in Section 10.5.
Splitting transformation
is the same as above, but for splitting transformations, i.e. those that can generate several sub-goals.
Menu Help
A very short online help, and some information about this software.

6.3.4  Preferences Dialog

The preferences dialog allows you to customize various settings. They are grouped together under several tabs.

General Settings tab
allows one to set various general settings.
Editors tab
allows one to customize the use of external editors for proof scripts.
Provers tab
allows to select which of the installed provers one wants to see as buttons in the left toolbar.
Uninstalled Provers tab
presents all the decision previously taken for missing provers, as described in Section 5.6. You can remove any recorded decision by clicking on it.

6.3.5  Displaying Counterexamples

When the selected prover finds (counterexample) model, it is possible to display parts of this model in the terms of the original Why3 input. Currently, this is supported for CVC4 prover version 1.5 and Z3.

To display the counterexample in Why3 IDE, the counterexample model generation must be enabled in File -/> Preferences -/> get counter-example. After running the prover and clicking on the prover result in, the counterexample can be displayed in the tab Counter-example. The counterexample is displayed with the original Why3 code in comments. Counterexample values for Why3 source code elements at given line are displayed in a comment at the line below. An alternative way how to display a counterexample is to use the option --get-ce of the prove command.

Why3 source code elements that should be a part of counterexample must be explicitly marked with "model" label. The following example shows a Why3 theory with some terms annotated with the model label and the generated counterexample in comments:

theory T use import int.Int goal g_no_lab_ex : forall x:int. x >= 42 -> x + 3 <= 50 goal g_lab_ex : forall x "model":int. ("model" x >= 42) -> ("model" "model_trace:x+3<=50" x + 3 <= 50) goal computation_ex : forall x1 "model" x2 "model" x3 "model" . (* x1 = 1; x2 = 1; x3 = 1 *) ("model" "model_trace: x1 + 1 = 2" x1 + 1 = 2) -> (* x1 + 1 = 2 = true *) ("model" x2 + 1 = 2) -> (* (= (+ x2 1) 2) = true *) ("model" x3 + 1 = 2) -> (* (= (+ x3 1) 2) = true *) ("model" x1 + x2 + x3 = 5) (* (= (+ (+ x1 x2) x3) 5) = false *)

To display counterexample values in assertions the term being asserted must be labeled with the label "model_vc". To display counterexample values in postconditions, the term in the postcondition must be labeled with the label "model_vc_post". The following example shows a counterexample of a function with postcondition:

let incr_ex ( x "model" : ref int ) (y "model" : ref int): unit (* x = -2; y = -2 *) ensures { !x = old !x + 2 + !y } = y := !y + 1; (* y = -1 *) x := !x + 1; (* x = -1 *) x := !x + 1 (* x = 0 *)

It is also possible to rename counterexample elements using the lable "model_trace:". The following example shows the use of renaming a counterexample element in order to print the counterexample in infix notation instead of default prefix notation:

goal g_lab_ex : forall x "model":int. ("model" x >= 42) -> (* x = 48; (<= 42 x) = true *) ("model" "model_trace:x+3<=50" x + 3 <= 50) (* x+3<=50 = false *)

Renaming counterexample elements is in particular useful when Why3 is used as intermediate language and to show names of counterexample elements in the source language instead of showing names of Why3 elements. Note that if the counterexample element is of a record type, it is also possible to rename names of the record fields by putting the label model_trace: to definitions of record fields. For example:

type r = {f "model_trace:.F" :int; g "model_trace:G" :bool}

When a prover is queried for a counterexample value of a term of an abstract type=, an internal representation of the value is get. To get the concrete representation, the term must be marked with the label "model_projected" and a projection function from the abstract type to a concrete type must be defined, marked as a projection using the meta "model_projection", and inlining of this function must be disabled using the meta "inline : no". The following example shows a counterexample of an abstract value:

theory A use import int.Int type byte function to_rep byte : int predicate in_range (x : int) = -128 <= x <= 127 axiom range_axiom : forall x:byte. in_range (to_rep x) meta "model_projection" function to_rep meta "inline : no" function to_rep goal abstr : forall x "model_projected" :byte. to_rep x >= 42 -> to_rep x + 3 <= 50 (* x = 48 *)

More examples of using counterexample feature of Why3 can be found in the file examples/tests/cvc4-models.mlw and examples/tests/cvc4-models.mlw. More information how counterexamples in Why3 works can be found in [6].

6.3.6  Additional Command-Line Options

The ide command also accepts the following options described for the command prove in Section 6.2.2.

--extra-expl-prefix <s>

6.4  The bench Command

The bench command adds a scheduler on top of the Why3 library. It is designed to compare various components of automatic proofs: automatic provers, transformations, definitions of a theory. For that purpose, it tries to prove predefined goals using each component to compare. Various formats can be used as outputs:

csv
the simpler and more informative format; the results are represented in an array; the rows correspond to the compared components, the columns correspond to the result (Valid, Unknown, Timeout, Failure, Invalid) and the CPU time taken in seconds.
average
it summarizes the number of the five different answers for each component. It also gives the average time taken.
timeline
for each component, it gives the number of valid goals along the time (10 slices between 0 and the longest time a component takes to prove a goal)

The compared components can be defined in an rc-file; examples/misc/prgbench.rc is an example of such a file. More generally, a bench configuration file looks like

[probs "myprobs"]
   file = "examples/mygoal.why" #relatives to the rc file
   file = "examples/myprogram.mlw"
   theory = "myprogram.T"
   goal = "mygoal.T.G"

   transform = "split_goal" #applied in this order
   transform = "..."
   transform = "..."

[tools "mytools"]
   prover = cvc3
   prover = altergo
   #or only one
   driver = "..."
   command = "..."

   loadpath = "..." #added to the one in why3.conf
   loadpath = "..."

   timelimit = 30
   memlimit = 300

   use = "toto.T" #use the theory toto (allow to add metas)

   transform = "simplify_array" #only 1 to 1 transformation

[bench "mybench"]
   tools = "mytools"
   tools = ...
   probs = "myprobs"
   probs = ...
   timeline = "prgbench.time"
   average = "prgbench.avg"
   csv = "prgbench.csv"

Such a file can define three families tools, probs, bench. A tools section defines a set of components to compare. A probs section defines a set of goals on which to compare some components. A bench section defines which components to compare using which goals. It refers by name to some sections tools and probs defined in the same file. The order of the definitions is irrelevant. Notice that one can use loadpath in a tools section to compare different axiomatizations.

One can run all the bench given in one bench configuration file with

why3 bench -B path_to_my_bench.rc

6.5  The replay Command

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

why3 replay [options] <project directory>

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.

Obsolete proofs

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.

Exit code and options

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:

-s
suppresses the output of the final tree view.
-q
runs quietly (no progress info).
--force
enforces saving the session, if all proof attempts replayed correctly, even if some goals are not proved.
--obsolete-only
replays the proofs only if the session contains obsolete proof attempts.
--smoke-detector {none|top|deep}
tries to detect if the context is self-contradicting.
--prover <prover>
restricts the replay to the selected provers only.
Smoke detector

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:

none
Do not run the smoke detector.
top
The negation of each proved goal is sent with the same timeout to the prover that proved the original goal.
  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.
deep
This is the same technique as top but the negation is pushed under the universal quantification (without changing them) and under the implication. The previous example becomes
  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.

6.6  The session Command

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:

info
prints informations and statistics about sessions.
latex
outputs session contents in LaTeX format.
html
outputs session contents in HTML format.
mod
modifies some of the proofs, selected by a filter.
copy
duplicates some of the proofs, selected by a filter.
copy-archive
same as copy but also archives the original proofs.
rm
removes some of the proofs, selected by a filter.

The first three commands do not modify the sessions, whereas the last four modify them. Only the proof attempts recorded are modified. No prover is called on the modified or created proof attempts, and consequently the proof status is always marked as obsolete.

6.6.1  Command info

The command why3 session info reports various informations about the session, depending on the following specific options.

--provers
prints the provers that appear inside the session, one by line.
--edited-files
prints all the files that appear in the session as edited proofs.
--stats
prints various proofs statistics, as detailed below.
--tree
prints the structure of the session as a tree in ASCII, as detailed below.
--print0
separates the results of the 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 coqwc
or 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
Session Tree

The hierarchical structure of the session is printed as a tree in ASCII. The files, theories, goals are marked with a question mark ?, if they are not verified. A proof is usually said to be verified if the proof result is valid and the proof is not obsolete. However here specially we separate these two properties. On the one hand if the proof suffers from an internal failure we mark it with an exclamation mark !, otherwise if it is not valid we mark it with a question mark ?, finally if it is valid we add nothing. On the other hand if the proof is obsolete we mark it with an O and if it is archived we mark it with an A.

For example, here are the session tree produced on the “hello proof” example of Section 1.

hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
                                                |    `-Alt-Ergo (0.94)
                                                |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
                                                |     |             |      `-Alt-Ergo (0.94)
                                                |     |             `-G2.1?-+-Coq (8.3pl4)?
                                                |     |                     |-Simplify (1.5.4)?
                                                |     |                     `-Alt-Ergo (0.94)?
                                                |     |-Simplify (1.5.4)?
                                                |     `-Alt-Ergo (0.94)?
                                                `-G1---Simplify (1.5.4)
Session Statistics

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 goals ==
  total: 5  proved: 3

== Goals not proved ==
  +-- file ../hello_proof.why
    +-- theory HelloProof
      +-- goal G2
        +-- transformation split_goal
          +-- goal G2.1

== Goals proved by only one prover ==
  +-- file ../hello_proof.why
    +-- theory HelloProof
      +-- goal G1: Simplify (1.5.4) (0.00)
      +-- goal G3: Alt-Ergo (0.94) (0.00)

== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
  Alt-Ergo (0.94)      :   2   0.00   0.00   0.00
  Simplify (1.5.4)     :   2   0.00   0.00   0.00

6.6.2  Command latex

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

-style <n>
sets output style (1 or 2, default 1) Option -style 2 produces an alternate version of LaTeX output, with a different layout of the tables.
-o <dir>
indicates where to produce LaTeX files (default: the session directory).
-longtable
uses the ‘longtable’ environment instead of ‘tabular’.
-e <elem>
produces a table for the given element, which is either a file, a theory or a root goal. The element must be specified using its path in dot notation, e.g. 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.
Customizing LaTeX output

The generated LaTeX files contain some macros that must be defined externally. Various definitions can be given to them to customize the output.

\provername
macro with one parameter, a prover name
\valid
macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
\noresult
macro without parameter, used where no result exists for the corresponding prover
\timeout
macro without parameter, used where the corresponding prover reached the time limit
\explanation
macro with one parameter, the goal name or its explanation

\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 6.1: Sample macros for the LaTeX command


Figure 6.2: LaTeX table produced for the HelloProof example (style 1)


Figure 6.3: LaTeX table produced for the HelloProof example (style 2)

Figure 6.1 suggests some definitions for these macros, while Figures 6.2 and 6.3 show the tables obtained from the HelloProof example of Section 1, respectively with style 1 and 2.

6.6.3  Command html

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 "HelloProof": not fully verified

ObligationsAlt-Ergo (0.94)Coq (8.3pl4)Simplify (1.5.4)
G1------0.00
G20.00---0.00
split_goal
  1.0.000.430.00
2.0.00---0.00
G30.00---0.00
Figure 6.4: 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 6.4 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.

--style <style>
sets the style to use, among simpletree and table; defaults to table.
-o <dir>
sets the directory where to output the produced files (‘-’ for stdout). The default is to output in the same directory as the session itself.
--context
adds context around the generated code in order to allow direct visualization (header, css, ...). It also adds in the output directory all the needed external files. It can’t be set with stdout output.
--add_pp <suffix> <cmd> <out_suffix>
sets a specific pretty-printer for files with the given suffix. Produced files use <out_suffix> as suffix. <cmd> must contain ‘%i’ which will be replaced by the input file and ‘%o’ which will be replaced by the output file.
--coqdoc
uses the coqdoc command to display Coq proof scripts. This is equivalent to --add_pp .v "coqdoc --no-index --html -o %o %i" .html

6.6.4  Commands modifying the proof attempts

The commands mod, copy, copy-archive, and rm, share the same set of options for selecting the proof attempts to work on:

--filter-prover <prover>
selects only the proof attempt with the given prover. This option can be specified multiple times in order to select all the proofs that corresponds to any of the given provers.
--filter-verified yes
selects only the proofs that are valid and not obsolete, while option --filter-verified no selects the ones that are not verified. --filter-verified all, the default, does not perform such a selection.
--filter-verified-goal yes
restricts the selection to the proofs of verified goals (that does not mean that the proof is verified). Same for the other cases no and all.
--filter-archived yes
restricts the selection to the proofs that are archived. Same for the other cases no and all except the default is no.

The commands mod, copy, and copy-archive, share the same set of options to specify the modification. The command mod modifies directly the proof attempt, copy copies the proof attempt before doing the modification, copy-archive marks the original proof attempt as archived. The options are:

--set-obsolete
marks the selected proofs as obsolete.
--set-archived
marks the selected proofs as archived.
--unset-archived
removes the archived attribute from the selected proofs.
--to-prover <prover>
modifies the prover, for example --to-prover Alt-Ergo,0.94. A conflict arises if a proof with this prover already exists. In this case, you can choose between four behaviors:

The command rm removes the selected proof attempts. The options --interactive, --force, and --conservative, can also be used to respectively ask before each suppression, suppress all the selected proofs (default), and remove only the proofs that are not verified. The macro option --clean corresponds to --filter-verified-goal --conservative and removes the proof attempts that are not verified but which correspond to verified goals.

The commands of this section do not accept by default to modify an obsolete session (as defined in 6.3.1). You need to add the option -F to force this behavior.

6.7  The doc Command

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.

Options
-o <dir>
defines the directory where to output the HTML files.
--output <dir>
is the same as -o.
--index
generates an index file index.html. This is the default behavior if more than one file is passed on the command line.
--no-index
prevents the generation of an index file.
--title <title>
sets title of the index page.
--stdlib-url <url>
sets a URL for files found in load path, so that links to definitions can be added.
Typesetting textual comments

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.

6.8  The execute Command

Why3 can symbolically execute programs written using the WhyML language (extension .mlw). See also Section 8.1.

6.9  The extract Command

Why3 can extract programs written using the WhyML language (extension .mlw) to OCaml. See also Section 8.2.

6.10  The realize Command

Why3 can produce skeleton files for proof assistants that, once filled, realize the given theories. See also Section 9.2.

6.11  The wc Command

Why3 can give some token statistics about Why3 and WhyML source codes.


Previous Up Next