manpages.tex 28 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
When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
Installation is performed (as super-user if needed) using
\begin{verbatim}
make install
\end{verbatim}
Installation can be tested as follows: 
\begin{enumerate}
\item install some external provers (see~Section\ref{provers} below)
\item run \texttt{why3config --detect}
\item run some examples from the distribution, \emph{e.g.} you should
obtain the following:
\begin{verbatim}
$ cd examples
$ why3replayer scottish-private-club
Info: found directory 'scottish-private-club' for the project
Opening session...[Xml warning] prolog ignored
[Reload] file '../scottish-private-club.why'
[Reload] theory 'ScottishClubProblem'
 done
Progress: 4/4
 1/1
Everything OK.
$ why3replayer programs/same_fringe
Info: found directory 'programs/same_fringe' for the project
Opening session...[Xml warning] prolog ignored
[Reload] file '../same_fringe.mlw'
[Reload] theory 'WP SameFringe'
[Reload] transformation split_goal for goal WP_parameter enum 
[Reload] transformation split_goal for goal WP_parameter eq_enum 
 done
Progress: 12/12
 3/3
Everything OK.
\end{verbatim}
\end{enumerate}
82

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

MARCHE Claude's avatar
MARCHE Claude committed
85 86
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
87 88 89 90
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
91
The \why executables are then available in the subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
92

MARCHE Claude's avatar
MARCHE Claude committed
93
\subsection{Installation of the \why library}
MARCHE Claude's avatar
MARCHE Claude committed
94 95
\label{sec:installlib}

MARCHE Claude's avatar
MARCHE Claude committed
96
By default, the \why library is not installed. It can be installed using
97 98 99 100
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
101

102
\section{Installation of external provers}\label{provers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
103

MARCHE Claude's avatar
MARCHE Claude committed
104 105
\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
106
them. There is no need to install these provers before compiling and
107
installing Why.
MARCHE Claude's avatar
add  
MARCHE Claude committed
108

MARCHE Claude's avatar
MARCHE Claude committed
109 110
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
111

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

MARCHE Claude's avatar
MARCHE Claude committed
115 116
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
117

MARCHE Claude's avatar
MARCHE Claude committed
118
\why must be configured to access external provers. Typically, this is done
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121 122 123 124 125 126
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
127
of the IDE. This must be redone each time a new prover is installed.
MARCHE Claude's avatar
MARCHE Claude committed
128

MARCHE Claude's avatar
MARCHE Claude committed
129
The provers which \why attempts to detect are described in
MARCHE Claude's avatar
MARCHE Claude committed
130
the readable configuration file \texttt{provers-detection-data.conf}
MARCHE Claude's avatar
MARCHE Claude committed
131
of the \why data directory (\eg{}
MARCHE Claude's avatar
MARCHE Claude committed
132 133 134 135 136
\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).

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

144
The provers which are typically looked for are
MARCHE Claude's avatar
MARCHE Claude committed
145
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
146 147 148 149 150 151
\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
152 153 154 155
\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
156
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
MARCHE Claude's avatar
MARCHE Claude committed
157
\end{itemize}
MARCHE Claude's avatar
add  
MARCHE Claude committed
158

MARCHE Claude's avatar
MARCHE Claude committed
159
\texttt{why3config} also detects the plugins installed in the \why
160 161 162 163 164
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,
165
\texttt{why3config} will only reset unset variables to default value,
166
but will not try to detect provers.
167
The option \texttt{--detect-provers} should be used to force
MARCHE Claude's avatar
MARCHE Claude committed
168
\why to detect again the available
169
provers and to replace them in the configuration file. The option
170
\texttt{--detect-plugins} will do the same for plugins.
171

MARCHE Claude's avatar
doc  
MARCHE Claude committed
172
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
173
\label{sec:why3ref}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
174

MARCHE Claude's avatar
MARCHE Claude committed
175 176
\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
177 178 179 180 181
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:
182
\begin{enumerate}
183
\item Parse the command line and report errors if needed.
184
\item Read the configuration file using the priority defined in
185 186 187 188
  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
189
  to obtain a set of \why theories for each file. It uses
190
  the filename extension or the \texttt{--format} option to choose
191
  among the available parsers. The \texttt{--list-format} option gives
192
  the list of registered parsers.
193
\item Extract the selected goals inside each of the selected theories
194 195
  into tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. The option
196
  \texttt{-T/--theory} applies to the last file appearing on the
197 198 199 200
  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.
201
\item Apply the transformation requested
202
  with \texttt{-a/--apply-transform} in their order of appearance on the
203 204 205 206
  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}
207
  option. \texttt{--list-provers} lists the known provers, i.e.~the ones
208
  which appear in the configuration file.
209 210 211 212
\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.
213 214
\end{enumerate}

215 216
%\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
217

218
The provers can answer the following output:
François Bobot's avatar
François Bobot committed
219
\begin{description}
François Bobot's avatar
François Bobot committed
220 221 222 223 224
\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
225
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
226
% \why can also be *)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
227 228 229 230 231 232
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)
233

François Bobot's avatar
François Bobot committed
234 235 236 237 238 239 240 241 242 243
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.

244
\section{The \texttt{why3ide} GUI}
MARCHE Claude's avatar
MARCHE Claude committed
245 246
\label{sec:ideref}

247 248 249 250
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
251 252 253 254 255 256
\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
257
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
258 259

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
260 261 262 263 264 265
\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
266 267 268 269
\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
270 271 272 273
\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
274
  expands it with this definition.
MARCHE Claude's avatar
MARCHE Claude committed
275

MARCHE Claude's avatar
MARCHE Claude committed
276 277 278 279 280 281 282 283 284
\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
285 286 287 288 289
\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
290

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

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

296 297 298
\item[Interrupt] Cancels all the proof attempts currently scheduled
  but not yet started.

MARCHE Claude's avatar
MARCHE Claude committed
299 300 301 302
\end{description}

\subsection{Menus}

303
\paragraph{Menu \textsf{File}}
MARCHE Claude's avatar
MARCHE Claude committed
304
\begin{description}
305
\item[Add File] adds a file in the GUI
MARCHE Claude's avatar
MARCHE Claude committed
306
%\item[Detect provers] runs provers auto-detection
307
\item[Preferences] opens a window for modifying preferred
308 309 310
  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.
311
\item[Quit] exits the GUI
MARCHE Claude's avatar
MARCHE Claude committed
312
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
313

314 315 316 317 318
\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
319 320
% \item[Hide proved goals] completely hides the proved rows of the tree
%   view [EXPERIMENTAL]
321 322 323
\end{description}

\paragraph{Menu \textsf{Tools}}
MARCHE Claude's avatar
MARCHE Claude committed
324 325 326 327 328
A copy of the tools already available in the left toolbar, plus:
\begin{itemize}
\item[Mark as obsolete] marks all the proof as obsolete. This allows to
  replay every proofs.
\end{itemize}
329 330 331 332

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

MARCHE Claude's avatar
MARCHE Claude committed
333 334
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
335 336 337 338 339 340
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
341
\item the maximal number of simultaneous provers allowed to run in parallel.
342 343 344 345 346 347 348
\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
349 350
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
351 352
\subsection{Structure of the database file}

353 354 355 356 357 358
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}
359 360 361

\section{The \texttt{why3ml} tool}

MARCHE Claude's avatar
MARCHE Claude committed
362 363
\texttt{why3ml} is an additional layer on \why library for
generating verification conditions from \whyml programs.
364 365
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
366
input files containing \whyml modules (see chapter~\ref{chap:whyml}
367 368 369 370 371 372 373 374 375
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
376

377
\section{The \texttt{why3bench} tool}
MARCHE Claude's avatar
MARCHE Claude committed
378

MARCHE Claude's avatar
MARCHE Claude committed
379
The \texttt{why3bench} tool adds a scheduler on top of the \why
380
library. \texttt{why3bench} is designed to compare various components
MARCHE Claude's avatar
MARCHE Claude committed
381 382 383 384
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
385
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
386
\item csv: the simpler and more informative format, the results are
François Bobot's avatar
François Bobot committed
387
  represented in an array, the rows corresponds to the
MARCHE Claude's avatar
MARCHE Claude committed
388 389 390 391 392 393 394
  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
395
\end{itemize}
396

MARCHE Claude's avatar
MARCHE Claude committed
397
The compared components can be defined in an \emph{rc-file},
MARCHE Claude's avatar
MARCHE Claude committed
398
\texttt{examples/programs/\ prgbench.rc} is such an example. More
MARCHE Claude's avatar
MARCHE Claude committed
399
generally a bench configuration file:
François Bobot's avatar
François Bobot committed
400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417
\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 = "..."

418
   loadpath = "..." #added to the one in why3.conf
François Bobot's avatar
François Bobot committed
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
   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}

438
Such a file can define three families \texttt{tools,probs,bench}. The
MARCHE Claude's avatar
MARCHE Claude committed
439 440 441 442
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
443 444
\texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
445
\texttt{tools} can be used to compare different axiomatizations.
François Bobot's avatar
François Bobot committed
446 447 448 449 450 451

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}
452

MARCHE Claude's avatar
MARCHE Claude committed
453
\section{The \texttt{why3replayer} tool}
454
\label{sec:why3replayer}
MARCHE Claude's avatar
MARCHE Claude committed
455 456 457

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
458 459 460
main goal is to play non-regression tests, \eg you can find in
\texttt{examples/regtests.sh} a script that runs regression tests on
all the examples.
MARCHE Claude's avatar
MARCHE Claude committed
461

MARCHE Claude's avatar
MARCHE Claude committed
462
The tool is invoked in a terminal or a script using
MARCHE Claude's avatar
MARCHE Claude committed
463 464 465 466 467 468
\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
469
the new run are shown.
MARCHE Claude's avatar
MARCHE Claude committed
470 471 472 473 474 475 476 477

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.

MARCHE Claude's avatar
MARCHE Claude committed
478 479 480 481 482 483
\paragraph{Obsolete proofs}

When some proofs store in the session file are obsolete, the replay is
attempt anyway, as for the replay button in the IDE. Then, if all the
replayed proofs went OK, the session file is updated, otherwise it is
not and you have to use the IDE to update it.
MARCHE Claude's avatar
MARCHE Claude committed
484 485

\paragraph{Exit code and options}
MARCHE Claude's avatar
MARCHE Claude committed
486

MARCHE Claude's avatar
MARCHE Claude committed
487 488 489 490
\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
MARCHE Claude's avatar
MARCHE Claude committed
491 492
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath
\item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.
493 494 495 496 497 498 499
\item option \texttt{-latex \textsl{<dir>}}: produce a summary of
  the replay under the form of a tabular environment in LaTeX, one
  tabular for each theory, one per file, in directory \texttt{\textsl{<dir>}}.
\item option \texttt{-latex2 \textsl{<dir>}}: alternate version of
  LaTeX output, with a different layout of the tables.
% \item option \texttt{-html \textsl{<file.html>}}: produce a summary of
%   the replay in HTML syntax.
MARCHE Claude's avatar
MARCHE Claude committed
500 501
\end{itemize}

502
\paragraph{Customizing LaTeX output}
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
503

504 505 506
The generated LaTeX files contain some macros that must be defined
externally.  Various definitions can be given to them to customize the
output. 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
507
\begin{itemize}
508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
\item \verb|\provername|: macro with one parameter, a prover name
\item \verb|\valid|: macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
\item \verb|\noresult|: macro without parameter, used where no result
  exists for the corresponding prover
\item \verb|\timeout|: macro without parameter, used where the corresponding prover reached the time limit
\item \verb|\explanation|: macro with one parameter, the goal name or its explnation
\end{itemize}

\begin{figure}[t]
  \begin{center}
    \input{HelloProof.tex}
  \end{center}
  \verbatiminput{./replayer_macros.tex}
  \caption{Sample macros for the LaTeX option of why3replayer}
\label{fig:replayer}
\end{figure}

Figure~\ref{fig:replayer} proposes some suggestions for these macros, together
with the table obtained from the hello proof example of Section~\ref{chap:starting}.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
527 528 529



Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
530

531
\section{The \texttt{why3.conf} configuration file}
532 533 534
\label{sec:whyconffile}


535
\begin{figure}[t]
536 537 538
\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
539
magic = 2
540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
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}
566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587
  \caption{Sample why3.conf file}
\label{fig:why3conf}
\end{figure}



One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
  \texttt{WHY3CONFIG} if set.
\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.
\end{itemize}
If none of these files exists, a built-in default configuration is used.

The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Figure~\ref{fig:why3conf}
shows an example of configuration file.
588

589 590
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
591 592 593 594 595
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.

596
Inside a section, one key can be associated with an integer (.eg -555),
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
597
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
598 599
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
600

601
\section{Drivers of External Provers}
602
\label{sec:drivers}
603 604 605 606 607 608 609

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
610 611

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
612
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
613

614 615 616 617
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.

618 619 620 621 622 623
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
624 625 626
\subsection{Non-splitting transformations}

\begin{description}
627

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

631 632
\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
633
\item[eliminate\_definition\_func]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
634
  Replaces all function definitions with axioms.
MARCHE Claude's avatar
MARCHE Claude committed
635
\item[eliminate\_definition\_pred]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
636 637 638 639 640 641 642
  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.
643

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
644 645 646
\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.
647

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

MARCHE Claude's avatar
MARCHE Claude committed
652
\item[eliminate\_if]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
653
  Apply both transformations above.
654

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

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

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

665
\item[eliminate\_let]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
666
  Apply both transformations above.
667

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
668 669 670
% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]
671

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

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
678 679 680 681 682 683 684 685
% \item[filter\_trigger] *)

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
687
\item[inline\_all]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
688 689 690 691 692
  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
693
\item[inline\_trivial]
694
  removes definitions of the form
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
695

696
\begin{verbatim}
697 698
function  f x_1 .. x_n = (g e_1 .. e_k)
predicate p x_1 .. x_n = (q e_1 .. e_k)
699
\end{verbatim}
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
700 701 702 703 704
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.
705

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
706 707
% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)
708

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
712 713
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
  then simplifies propositional structure: removes true, false, ``f
714
  and f'' to ``f'', etc.
715 716 717

\item[simplify\_recursive\_definition] reduces mutually recursive
  definitions if they are not really mutually recursive, e.g.:
718
\begin{verbatim}
719
function f : ... = .... g ...
720 721 722 723 724

with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
725 726
function g : .. = e
function f : ... = .... g ...
727 728 729
\end{verbatim}
if f does not occur in e

MARCHE Claude's avatar
MARCHE Claude committed
730
\item[simplify\_trivial\_quantification]
731 732 733 734 735 736 737 738 739
  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
740
  into
741 742 743 744 745
\begin{verbatim}
P(t)
\end{verbatim}
  More generally, it applies this simplification whenever x=t appear
  in a negative position.
746

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

MARCHE Claude's avatar
MARCHE Claude committed
750
\item[split\_premise]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
751
  splits conjunctive premises.
752

MARCHE Claude's avatar
MARCHE Claude committed
753 754 755 756 757
\end{description}

\subsection{Splitting transformations}

\begin{description}
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
758 759 760 761 762 763 764 765 766 767 768

\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
769
\item[split\_all]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
770
  composition of \texttt{split\_premise} and \texttt{split\_goal}.
771 772

\item[split\_goal] if the goal is a conjunction of goals, returns the
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
773 774 775 776 777 778
  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
779 780
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
781

MARCHE Claude's avatar
doc  
MARCHE Claude committed
782 783 784 785 786 787

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