manpages.tex 25.2 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
\chapter{Reference manuals for the \why tools}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:manpages}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
3
4

\section{Compilation, Installation}
MARCHE Claude's avatar
MARCHE Claude committed
5
\label{sec:install}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
Compilation of \why must start with a configuration phase which is run as
MARCHE Claude's avatar
MARCHE Claude committed
8
9
10
\begin{verbatim}
./configure
\end{verbatim}
11
This analyzes your current configuration and checks if requirements hold.
MARCHE Claude's avatar
MARCHE Claude committed
12
13
Compilation requires:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
14
15
\item The Objective Caml compiler, version 3.10 or higher. It is
  available as a binary package for most Unix distributions. For
16
  Debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
17
18
19
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
20
It is also installable from sources, downloadable from the site
MARCHE Claude's avatar
MARCHE Claude committed
21
\url{http://caml.inria.fr/ocaml/}
MARCHE Claude's avatar
add    
MARCHE Claude committed
22
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
MARCHE Claude committed
24
For some tools, additional OCaml libraries are needed:
MARCHE Claude's avatar
add    
MARCHE Claude committed
25
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
26
27
28
\item For the IDE: the Lablgtk2 library for OCaml bindings of the gtk2
  graphical library. For Debian-based Linux distributions, you can
  install the packages
MARCHE Claude's avatar
MARCHE Claude committed
29
30
31
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
32
33
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
MARCHE Claude's avatar
MARCHE Claude committed
34

MARCHE Claude's avatar
MARCHE Claude committed
35
\item For \texttt{why3bench}: The OCaml bindings of the sqlite3 library.
36
For Debian-based Linux distributions, you can install the package
MARCHE Claude's avatar
MARCHE Claude committed
37
38
39
40
41
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
MARCHE Claude's avatar
MARCHE Claude committed
42
43
\end{itemize}

44
45
46
47
48
When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}

MARCHE Claude's avatar
add    
MARCHE Claude committed
49
50
\subsection{Local use, without installation}

MARCHE Claude's avatar
MARCHE Claude committed
51
52
It is not mandatory to install \why into system directories.
\why can be configured and compiled for local use as follows:
MARCHE Claude's avatar
add    
MARCHE Claude committed
53
54
55
56
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
57
The \why executables are then available in the subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
58

MARCHE Claude's avatar
MARCHE Claude committed
59
\subsection{Installation of the \why library}
MARCHE Claude's avatar
MARCHE Claude committed
60
61
\label{sec:installlib}

MARCHE Claude's avatar
MARCHE Claude committed
62
By default, the \why library is not installed. It can be installed using
63
64
65
66
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
67

MARCHE Claude's avatar
MARCHE Claude committed
68
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
69

MARCHE Claude's avatar
MARCHE Claude committed
70
71
\why can use a wide range of external theorem provers. These need to
be installed separately, and then \why needs to be configured to use
MARCHE Claude's avatar
MARCHE Claude committed
72
them. There is no need to install these provers before compiling and
73
installing Why.
MARCHE Claude's avatar
add    
MARCHE Claude committed
74

MARCHE Claude's avatar
MARCHE Claude committed
75
76
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
77

MARCHE Claude's avatar
MARCHE Claude committed
78
For configuring \why to use the provers, follow instructions given in
MARCHE Claude's avatar
MARCHE Claude committed
79
Section~\ref{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
80

MARCHE Claude's avatar
MARCHE Claude committed
81
82
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
83

MARCHE Claude's avatar
MARCHE Claude committed
84
\why must be configured to access external provers. Typically, this is done
MARCHE Claude's avatar
MARCHE Claude committed
85
86
87
88
89
90
91
92
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
93
of the IDE. This must be redone each time a new prover is installed.
MARCHE Claude's avatar
MARCHE Claude committed
94

MARCHE Claude's avatar
MARCHE Claude committed
95
The provers which \why attempts to detect are described in
MARCHE Claude's avatar
MARCHE Claude committed
96
the readable configuration file \texttt{provers-detection-data.conf}
MARCHE Claude's avatar
MARCHE Claude committed
97
of the \why data directory (\eg{}
MARCHE Claude's avatar
MARCHE Claude committed
98
99
100
101
102
\texttt{/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).

103
The result of provers detection is stored in the user's
104
105
configuration file (\verb+~/.why3.conf+ or, in the case of local
installation, \verb+why3.conf+ in Why3 sources top directory). This file
106
is also human-readable, and advanced users may modify it in order to
107
experiment with different ways of calling provers, \eg{} different
108
versions of the same prover, or with different options.
MARCHE Claude's avatar
MARCHE Claude committed
109

110
The provers which are typically looked for are
MARCHE Claude's avatar
MARCHE Claude committed
111
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
112
113
114
115
116
117
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
\item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
\item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
MARCHE Claude's avatar
MARCHE Claude committed
118
119
120
121
\item Spass: \url{http://www.spass-prover.org/}
\item Vampire: \url{http://www.voronkov.com/vampire.cgi}
\item VeriT: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}, only versions 1.xx since versions 2.xx do not support quantifiers
MARCHE Claude's avatar
MARCHE Claude committed
122
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
MARCHE Claude's avatar
MARCHE Claude committed
123
\end{itemize}
MARCHE Claude's avatar
add    
MARCHE Claude committed
124

MARCHE Claude's avatar
MARCHE Claude committed
125
\texttt{why3config} also detects the plugins installed in the \why
126
127
128
129
130
plugins directory (\eg{} \texttt{/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,
131
\texttt{why3config} will only reset unset variables to default value,
132
but will not try to detect provers.
133
The option \texttt{--detect-provers} should be used to force
MARCHE Claude's avatar
MARCHE Claude committed
134
\why to detect again the available
135
provers and to replace them in the configuration file. The option
136
\texttt{--detect-plugins} will do the same for plugins.
137

MARCHE Claude's avatar
doc    
MARCHE Claude committed
138
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
139
\label{sec:why3ref}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
140

MARCHE Claude's avatar
MARCHE Claude committed
141
142
\why is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
143
144
145
146
147
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.

The \texttt{why3} tool executes the following steps:
148
\begin{enumerate}
149
\item Parse the command line and report errors if needed.
150
\item Read the configuration file using the priority defined in
151
152
153
154
  Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
  stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
MARCHE Claude's avatar
MARCHE Claude committed
155
  to obtain a set of \why theories for each file. It uses
156
  the filename extension or the \texttt{--format} option to choose
157
  among the available parsers. The \texttt{--list-format} option gives
158
  the list of registered parsers.
159
\item Extract the selected goals inside each of the selected theories
160
161
  into tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. The option
162
  \texttt{-T/--theory} applies to the last file appearing on the
163
164
165
166
  command line, the option \texttt{-G/--goal} applies to the last 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.
167
\item Apply the transformation requested
168
  with \texttt{-a/--apply-transform} in their order of appearance on the
169
170
171
172
  command line. \texttt{--list-transforms} list the known
  transformations, plugins can add more of them.
\item Apply the driver selected with the \texttt{-D/--driver} option,
  or the driver of the prover selected with \texttt{-P/--prover}
173
  option. \texttt{--list-provers} lists the known provers, i.e.~the ones
174
  which appear in the configuration file.
175
176
177
178
\item If the option \texttt{-P/--prover} is given, call the selected prover
  on each generated task and print the results. If the option
  \texttt{-D/--driver} is given, print each generated task using
  the format specified in the selected driver.
179
180
\end{enumerate}

181
182
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently.  *)
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
183

184
The provers can answer the following output:
François Bobot's avatar
François Bobot committed
185
\begin{description}
François Bobot's avatar
François Bobot committed
186
187
188
189
190
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover stop by itself to search,
\item[Timeout] the prover doesn't have enough time,
\item[Failure] an error occured,
\item[Invalid] the prover know the goal can't be proved
François Bobot's avatar
François Bobot committed
191
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
192
% \why can also be *)
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
193
194
195
196
197
198
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)
199

François Bobot's avatar
François Bobot committed
200
201
202
203
204
205
206
207
208
209
The option \texttt{--bisect} change the behaviors of why3. With this
option, \texttt{-P/--prover} and \texttt{-o/--output} must be given
and a valid goal must be selected. The last step executed by why3 is
replaced by computing a minimal set (in the great majority of the
case) of declarations which still prove the goal. Currently it doesn't
use any information provided by the prover, it call the prover
multiple time with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \texttt{-o/--output} option.

210
\section{The \texttt{why3ide} GUI}
MARCHE Claude's avatar
MARCHE Claude committed
211
212
\label{sec:ideref}

213
214
215
216
The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.

MARCHE Claude's avatar
MARCHE Claude committed
217
218
219
220
221
222
\subsection{Command-line options}

\begin{description}
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
223
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
224
225

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
226
227
228
229
230
231
\item[Context] 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.

MARCHE Claude's avatar
MARCHE Claude committed
232
233
234
235
\item[Provers] To each detected prover corresponds to a button in this
  prover framed box. Clicking on this button starts the prover on the
  selected goal(s).

MARCHE Claude's avatar
MARCHE Claude committed
236
237
238
239
\item[Split] This splits the current goal into subgoals if it is a
  conjunction of two or more goals.

\item[Inline] If the goal is headed by a defined predicate symbol,
MARCHE Claude's avatar
MARCHE Claude committed
240
  expands it with this definition.
MARCHE Claude's avatar
MARCHE Claude committed
241

MARCHE Claude's avatar
MARCHE Claude committed
242
243
244
245
246
247
248
249
250
\item[Edit] Start 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.

MARCHE Claude's avatar
MARCHE Claude committed
251
252
253
254
255
\item[Replay] Replay all 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.
MARCHE Claude's avatar
MARCHE Claude committed
256

257
\item[Remove] Removes a proof attempt or a transformation.
MARCHE Claude's avatar
MARCHE Claude committed
258

MARCHE Claude's avatar
MARCHE Claude committed
259
260
261
\item[Clean] Removes any unsuccessful proof attempt for which there is
  another successful proof attempt for the same goal

MARCHE Claude's avatar
MARCHE Claude committed
262
263
264
265
\end{description}

\subsection{Menus}

266
\paragraph{Menu \textsf{File}}
MARCHE Claude's avatar
MARCHE Claude committed
267
\begin{description}
268
\item[Add File] adds a file in the GUI
MARCHE Claude's avatar
MARCHE Claude committed
269
%\item[Detect provers] runs provers auto-detection
270
\item[Preferences] opens a window for modifying preferred
271
272
273
  configuration parameters, see details below
\item[Reload] reloads the input files from disk, and update the session state accordingly
\item[Save session] Save current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
274
\item[Quit] exits the GUI
MARCHE Claude's avatar
MARCHE Claude committed
275
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
276

277
278
279
280
281
\paragraph{Menu \textsf{View}}
\begin{description}
\item[Expand All] expands all the rows of the tree view
\item[Collapse proved goals] closes all the rows of the tree view
  which are proved.
MARCHE Claude's avatar
MARCHE Claude committed
282
283
% \item[Hide proved goals] completely hides the proved rows of the tree
%   view [EXPERIMENTAL]
284
285
286
287
288
289
290
291
\end{description}

\paragraph{Menu \textsf{Tools}}
A copy of the tools already available in the left toolbar

\paragraph{Menu \textsf{Help}}
A very short online help, and some information about this software.

MARCHE Claude's avatar
MARCHE Claude committed
292
293
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
294
295
296
297
298
299
The preferences window allows you customize
\begin{itemize}
\item the default editor to use when the \textsf{Edit} button is
  pressed. This might be overidden for a specific prover (the only way
  to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
300
\item the maximal number of simultaneous provers allowed to run in parallel.
301
302
303
304
305
306
307
\item The policy for saving session:
  \begin{itemize}
  \item always save on exit (default): the current state of the proof session is saving on exit
  \item never save on exit: the current state of the session is never save automatically, you must use menu \textsf{File/Save session} to save when wanted
  \item ask whether to save: on exit, a popup window ask whether you
    want to save or not.
  \end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
308
309
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
310
311
\subsection{Structure of the database file}

312
313
314
315
316
317
The session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.

The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
\verbatiminput{../share/why3session.dtd}
318
319
320

\section{The \texttt{why3ml} tool}

MARCHE Claude's avatar
MARCHE Claude committed
321
322
\texttt{why3ml} is an additional layer on \why library for
generating verification conditions from \whyml programs.
323
324
The command-line of \texttt{why3ml} is identical to that of
\texttt{why3}, but also accepts files with extension \texttt{.mlw} as
MARCHE Claude's avatar
MARCHE Claude committed
325
input files containing \whyml modules (see chapter~\ref{chap:whyml}
326
327
328
329
330
331
332
333
334
and section~\ref{sec:syntax:whyml}). Modules are turned into
theories containing verification conditions as goals, and then
\texttt{why3ml} behaves exactly as \texttt{why3} for the remaining of
the process.
Note that files with extension \texttt{.mlw} can also be loaded in
\texttt{why3ide}.

For those who want to experiment with \whyml, many examples are provided in
\texttt{examples/programs}.
MARCHE Claude's avatar
doc    
MARCHE Claude committed
335

336
\section{The \texttt{why3bench} tool}
MARCHE Claude's avatar
MARCHE Claude committed
337

MARCHE Claude's avatar
MARCHE Claude committed
338
The \texttt{why3bench} tool adds a scheduler on top of the \why
339
library. \texttt{why3bench} is designed to compare various components
MARCHE Claude's avatar
MARCHE Claude committed
340
341
342
343
of automatic proofs: automatic provers, transformations, definitions
of a theory. For that goal it tries to prove predefined goals using
each component to compare. \texttt{why3bench} allows to output the
comparison in various formats:
François Bobot's avatar
François Bobot committed
344
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
345
\item csv: the simpler and more informative format, the results are
François Bobot's avatar
François Bobot committed
346
  represented in an array, the rows corresponds to the
MARCHE Claude's avatar
MARCHE Claude committed
347
348
349
350
351
352
353
  compared components, the columns correspond to the result
  (Valid,Unknown,Timout,Failure,Invalid) and the CPU time taken in seconds.
\item average: summarizes the number of the five different answers
  for each component. It also gives the average time taken.
\item 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)
François Bobot's avatar
François Bobot committed
354
\end{itemize}
355

MARCHE Claude's avatar
MARCHE Claude committed
356
The compared components can be defined in an \emph{rc-file},
MARCHE Claude's avatar
MARCHE Claude committed
357
\texttt{examples/programs/\ prgbench.rc} is such an example. More
MARCHE Claude's avatar
MARCHE Claude committed
358
generally a bench configuration file:
François Bobot's avatar
François Bobot committed
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
\begin{verbatim}
[probs "myprobs"]
   file = "examples/monbut.why" #relatives to the rc file
   file = "examples/monprogram.mlw"
   theory = "monprogram.T"
   goal = "monbut.T.G"

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

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

377
   loadpath = "..." #added to the one in why3.conf
François Bobot's avatar
François Bobot committed
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
   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"
\end{verbatim}

397
Such a file can define three families \texttt{tools,probs,bench}. The
MARCHE Claude's avatar
MARCHE Claude committed
398
399
400
401
sections \texttt{tools} define a set of components to compare, the
sections \texttt{probs} define a set of goals on which to compare some
components and the sections \texttt{bench} define which components to
compare using which goals. It refers by name to the sections
François Bobot's avatar
François Bobot committed
402
403
\texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
404
\texttt{tools} can be used to compare different axiomatizations.
François Bobot's avatar
François Bobot committed
405
406
407
408
409
410

One can run all the bench given in one bench configuration file with
\texttt{why3bench} :
\begin{verbatim}
why3bench -B path_to_my_bench.rc
\end{verbatim}
411

MARCHE Claude's avatar
MARCHE Claude committed
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
\section{The \texttt{why3replayer} tool}

The purpose of the \texttt{why3replayer} tool is to execute the proofs
stored in a \why session file, as the one produced by the IDE. Its
main goal is to play non-regression tests.

The tool is inkoved in a terminal or a script using
\begin{flushleft}\ttfamily
  why3replayer \textsl{[options] <project directory>}
\end{flushleft}
The session file \texttt{why3session.xml} stored in the given
directory is loaded and all the proofs it contains are rerun. Then,
any difference 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, independently
of the fact the considered goal is proved or not. When all the proof
runs 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'', that is when a goal, a theory or a file is
fully proved the subtree is not shown.

For example, running the replayer on the \texttt{hello\_proof} example
of Section~\ref{chap:starting} is as follows.
\begin{verbatim}
$ why3replayer hello_proof
Info: found directory 'hello_proof' for the project
Opening session...[Xml warning] prolog ignored
[Reload] file '../hello_proof.why'
[Reload] theory 'HelloProof'
[Reload] transformation split_goal for goal G2
 done
Progress: 9/9
 2/3
   +--file ../hello_proof.why: 2/3
      +--theory HelloProof: 2/3
         +--goal G2 not proved
Everything OK.
\end{verbatim}
The last line tells us that no difference was detected between the
current run and the informations in the XML file. The tree above
reminds us that the G2 is not proved.

\paragraph{Exit code and options}
\begin{itemize}
\item The exit code is 0 if no difference was detected, 1 if there
  was. Other exit codes mean some failure in running the replay.
\item option \texttt{-s}: suppresses the output of the final tree view
\item option \texttt{-I \textsl{<path>}}: suppresses the output of the final tree view
\end{itemize}

463
\section{The \texttt{why3.conf} configuration file}
464
\label{sec:whyconffile}
465
466
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
467
468
user's configuration file to consider:
\begin{itemize}
469
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
470
\item the file specified by the environment variable
471
  \texttt{WHY3CONFIG} if set.
472
473
474
\item the file \texttt{\$HOME/.why3.conf}
  (\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
  local installation, \texttt{why3.conf} in Why3 sources top directory.
475
\end{itemize}
476
If none of these files exists, a built-in default configuration is used.
477

478
479
480
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Here follows an example of
configuration file.
481
482
483
484

\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
485
magic = 2
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
memlimit = 0
running_provers_max = 2
timelimit = 10

[ide ]
default_editor = "emacs"
task_height = 384
tree_width = 438
verbose = 0
window_height = 779
window_width = 638

[prover coq]
command = "coqc %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
name = "Coq"
version = "8.2pl2"

[prover alt-ergo]
command = "why3-cpulimit %t %m alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo.drv"
editor = ""
name = "Alt-Ergo"
version = "0.91"
\end{verbatim}

513
514
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
515
516
517
518
519
section can be only one identifier, \texttt{main} and \texttt{ide} in
the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.

520
Inside a section, one key can be associated with an integer (.eg -555),
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
521
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
522
523
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
MARCHE Claude's avatar
MARCHE Claude committed
524

525
\section{Drivers of External Provers}
526
\label{sec:drivers}
527
528
529
530
531
532
533

The drivers of external provers are readable files, in directory
\texttt{drivers}. Experimented users can modify them to change the way
the external provers are called, in particular which transformations
are applied to goals.

[TO BE COMPLETED LATER]
MARCHE Claude's avatar
MARCHE Claude committed
534
535

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
536
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
537

538
539
540
541
Here is a quick documentation of provided transformations. We give
first the non-splitting ones, \eg{} those which produce one goal as
result, and others which produces any number of goals.

542
543
544
545
546
547
Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}

MARCHE Claude's avatar
MARCHE Claude committed
548
549
550
\subsection{Non-splitting transformations}

\begin{description}
551

MARCHE Claude's avatar
MARCHE Claude committed
552
553
\item[eliminate\_algebraic] Replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}
554

555
556
\item[eliminate\_builtin] Suppress definitions of symbols which are
  declared as builtin in the driver, i.e. with a ``syntax'' rule.
MARCHE Claude's avatar
MARCHE Claude committed
557
\item[eliminate\_definition\_func]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
558
  Replaces all function definitions with axioms.
MARCHE Claude's avatar
MARCHE Claude committed
559
\item[eliminate\_definition\_pred]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
560
561
562
563
564
565
566
  Replaces all predicate definitions with axioms.
\item[eliminate\_definition]
  Apply both transformations above.
\item[eliminate\_mutual\_recursion]
  Replaces mutually recursive definitions with axioms.
\item[eliminate\_recursion]
  Replaces all recursive definitions with axioms.
567

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
568
569
570
\item[eliminate\_if\_term] replaces terms of the form \texttt{if
    formula then t2 else t3} by lifting them at the level of formulas.
  This may introduce \texttt{if then else } in formulas.
571

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
572
573
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
  else f3} by an equivalent formula using implications and other
574
  connectives.
575

MARCHE Claude's avatar
MARCHE Claude committed
576
\item[eliminate\_if]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
577
  Apply both transformations above.
578

579
\item[eliminate\_inductive] replaces inductive predicates by
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
580
581
  (incomplete) axiomatic definitions, i.e. construction axioms and
  an inversion axiom.
582

MARCHE Claude's avatar
MARCHE Claude committed
583
\item[eliminate\_let\_fmla]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
584
585
  Eliminates \texttt{let} by substitution, at the predicate level.

MARCHE Claude's avatar
MARCHE Claude committed
586
\item[eliminate\_let\_term]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
587
588
  Eliminates \texttt{let} by substitution, at the term level.

589
\item[eliminate\_let]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
590
  Apply both transformations above.
591

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
592
593
594
% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]
595

MARCHE Claude's avatar
MARCHE Claude committed
596
\item[encoding\_smt]
597
598
  Encode polymorphic types into monomorphic type~\cite{conchon08smt}.

MARCHE Claude's avatar
MARCHE Claude committed
599
\item[encoding\_tptp]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
600
  Encode theories into unsorted logic. %~\cite{cruanes10}.
601

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
602
603
604
605
606
607
608
609
% \item[filter\_trigger] *)

% \item[filter\_trigger\_builtin] *)

% \item[filter\_trigger\_no\_predicate] *)

% \item[hypothesis\_selection] *)
%   Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *)
610

MARCHE Claude's avatar
MARCHE Claude committed
611
\item[inline\_all]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
612
613
614
615
616
  expands all non-recursive definitions.

\item[inline\_goal] Expands all outermost symbols of the goal that
  have a non-recursive definition.

MARCHE Claude's avatar
MARCHE Claude committed
617
\item[inline\_trivial]
618
  removes definitions of the form
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
619

620
\begin{verbatim}
621
622
function  f x_1 .. x_n = (g e_1 .. e_k)
predicate p x_1 .. x_n = (q e_1 .. e_k)
623
\end{verbatim}
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
624
625
626
627
628
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$

\item[introduce\_premises] moves antecedents of implications and
  universal quantifications of the goal into the premises of the task.
629

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
630
631
% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)
632

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
633
634
\item[simplify\_array] Automatically rewrites the task using the lemma
  \verb|Select_eq| of theory \verb|array.Array|.
635

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
636
637
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
  then simplifies propositional structure: removes true, false, ``f
638
  and f'' to ``f'', etc.
639
640
641

\item[simplify\_recursive\_definition] reduces mutually recursive
  definitions if they are not really mutually recursive, e.g.:
642
\begin{verbatim}
643
function f : ... = .... g ...
644
645
646
647
648

with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
649
650
function g : .. = e
function f : ... = .... g ...
651
652
653
\end{verbatim}
if f does not occur in e

MARCHE Claude's avatar
MARCHE Claude committed
654
\item[simplify\_trivial\_quantification]
655
656
657
658
659
660
661
662
663
  simplifies quantifications of the form
\begin{verbatim}
  forall x, x=t -> P(x)
\end{verbatim}
or
\begin{verbatim}
  forall x, t=x -> P(x)
\end{verbatim}
  when x does not occur in t
664
  into
665
666
667
668
669
\begin{verbatim}
P(t)
\end{verbatim}
  More generally, it applies this simplification whenever x=t appear
  in a negative position.
670

MARCHE Claude's avatar
MARCHE Claude committed
671
\item[simplify\_trivial\_quantification\_in\_goal]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
672
  same as above but applies only in the goal.
673

MARCHE Claude's avatar
MARCHE Claude committed
674
\item[split\_premise]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
675
  splits conjunctive premises.
676

MARCHE Claude's avatar
MARCHE Claude committed
677
678
679
680
681
\end{description}

\subsection{Splitting transformations}

\begin{description}
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
682
683
684
685
686
687
688
689
690
691
692

\item[full\_split\_all]
  composition of \texttt{split\_premise} and \texttt{full\_split\_goal}.

\item[full\_split\_goal] puts the goal in a conjunctive form,
  returns the corresponding set of subgoals. The number of subgoals
  generated may be exponential in the size of the initial goal.

\item[simplify\_formula\_and\_task] same as \texttt{simplify\_formula}
  but also removes the goal if it is equivalent to true.

MARCHE Claude's avatar
MARCHE Claude committed
693
\item[split\_all]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
694
  composition of \texttt{split\_premise} and \texttt{split\_goal}.
695
696

\item[split\_goal] if the goal is a conjunction of goals, returns the
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
697
698
699
700
701
702
  corresponding set of subgoals. The number of subgoals generated is linear in
  the size of the initial goal.

\item[split\_intro]
  when a goal is an implication, moves the antecedents into the premises.

MARCHE Claude's avatar
MARCHE Claude committed
703
704
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
705

MARCHE Claude's avatar
doc    
MARCHE Claude committed
706
707
708
709
710
711

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: