Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

manpages.tex 15.7 KB
Newer Older
MARCHE Claude's avatar
doc  
MARCHE Claude committed
1
\chapter{Reference manuals for the Why3 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 8 9 10 11 12 13
Compilation of Why3 must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes you current configuration and check if requirements hold.
Compilation requires:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
14 15 16
\item The Objective Caml compiler, version 3.10 or higher. It is
  available as a binary package for most Unix distributions. For
  debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
It is also installable from sources, downloadable from the Web site
\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
add  
MARCHE Claude committed
24 25
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29 30 31 32
\item The Lablgtk2 library for Ocaml bindings of the gtk2 graphical library.
 For debian-based Linux distributions, you can install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
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
33 34 35 36 37 38 39
\item The Ocaml bindings of the sqlite3 library
For debian-based Linux distributions, you can install the package
\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
40 41
\end{itemize}

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

MARCHE Claude's avatar
MARCHE Claude committed
44
It is not mandatory to install Why3 to use it. Local use is obtained via
MARCHE Claude's avatar
add  
MARCHE Claude committed
45 46 47 48
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
49
The Why3 executables are then available in subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
50

MARCHE Claude's avatar
MARCHE Claude committed
51 52 53
\subsection{Installation of the Why3 library}
\label{sec:installlib}

54 55 56 57 58
By default, the Why3 library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
59

MARCHE Claude's avatar
MARCHE Claude committed
60
\section{Installation of external provers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
61

MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65
Why3 can use a wide range of external theorem provers. These need to
be installed separately, and then Why3 needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why. 
MARCHE Claude's avatar
add  
MARCHE Claude committed
66

MARCHE Claude's avatar
MARCHE Claude committed
67 68
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
69

MARCHE Claude's avatar
MARCHE Claude committed
70 71
For configuring Why3 to use the provers, follow intructions given in
Section~\ref{sec:why3config}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
72

MARCHE Claude's avatar
MARCHE Claude committed
73 74
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
75

MARCHE Claude's avatar
MARCHE Claude committed
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
Why3 must be configured to access external provers. Typically, this is done
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
of the IDE. This must be done again each time a new prover is installed.

The set of all provers which are attempted to detect is described in
the readable configuration file \texttt{provers-detection-data.conf}
of the Why3 data directory (\eg{}
\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).

The result of the prover detection is stored in the user's
configuration file (\eg{} \texttt{~/.why.conf}). Again, this file is
human readable, and advanced users may modify it in order to
experiment different ways of calling provers, \eg{} different versions
of the same prover, or with different options.

The provers which are typically attemped for detection are
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106 107 108 109 110 111 112
\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/}
\item Spass~: \url{http://www.spass-prover.org/}
\item veriT~: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
MARCHE Claude's avatar
MARCHE Claude committed
113
\end{itemize}
MARCHE Claude's avatar
add  
MARCHE Claude committed
114

MARCHE Claude's avatar
MARCHE Claude committed
115
\texttt{why3config} also detects the plugins installed in the Why3
116 117 118 119 120 121
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,
\texttt{why3config} will only reset unset variables to default value.
MARCHE Claude's avatar
MARCHE Claude committed
122
The option \texttt{--autodetect-provers} will detect again the available
123
provers and will replace them in the file configuration.
MARCHE Claude's avatar
MARCHE Claude committed
124
\texttt{--autodetect-plugins} will do the same for plugins.
125

MARCHE Claude's avatar
doc  
MARCHE Claude committed
126
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
127
\label{sec:why3ref}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
128

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
Why3 is primarily used to call provers on goals contains by file in
why3 format \texttt{.why} extension. However plugins can register
parser which can extend the known format. \texttt{why3ml} apply the
following steps :
\begin{enumerate}
\item Parse the command line and report error if needed
\item Read the configuration file using the priority defined in
  section\ref{sec:whyconffile}
\item Load the plugins mentionned in the configuration. It will not
  stop if a plugin fail to load.
\item Parse and type the given files using the correct parser in order
  to obtain a set of why theory for each files. It uses
  the filename extension or the \texttt{--format} options to choose
  among the available parsers. \texttt{--list-format} gives the list
  of them.
\item Extract the selected goals inside each selected theories into
  tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. One
  \texttt{-T/--theory} applies to the last file appearing on the
  commandline, one \texttt{-G/--goal} applies to the last theory
  appearing on the commandline. If none theories are selected in one
  file, they are all selected. If none goals are selected inside one
  selected theory, they are all selected.
\item Apply the transformation requested
  with \texttt{-a/--apply-transform} in the order they appear on the
  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}
  option. \texttt{--list-provers} lists the known provers, ie the one
  which appear in the configuration file.
\item Print the result of the standard output if \texttt{-D/--driver}
  is used or call the prover and print the result if
  \texttt{-P/--prover} is used.
\end{enumerate}

\texttt{why3} call the prover sequentially, use \texttt{why3bench} if
you want to call the provers concurrently. \texttt{Why3} can also be
used to provide other informations :
\begin{itemize}
\item \texttt{print-namespace} print the namespace of the selected
  theories
171
\item [TO BE COMPLETED]
172 173
\end{itemize}

174
\section{The \texttt{why3ide} GUI}
MARCHE Claude's avatar
MARCHE Claude committed
175 176
\label{sec:ideref}

177 178 179 180
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
181 182 183 184 185 186
\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
187
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
188 189

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
190 191 192 193 194 195
\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
196 197 198 199
\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
200 201 202 203 204 205
\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,
  expands it with this definition. [NOT YET AVAILABLE]

MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209 210 211 212 213 214
\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
215 216
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]

MARCHE Claude's avatar
MARCHE Claude committed
217 218
\item[Remove] Remove a proof attempt or a transformation. 
  [Removing transformation NOT YET AVAILABLE]
MARCHE Claude's avatar
MARCHE Claude committed
219 220 221 222 223 224

\end{description}

\subsection{Menus}

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
225 226
\item[File/Detect provers] runs provers auto-detection
\item[File/Preferences] opens a window for modifying preferred configuration
MARCHE Claude's avatar
MARCHE Claude committed
227
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
228

MARCHE Claude's avatar
MARCHE Claude committed
229 230
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
231 232 233 234 235 236 237 238 239
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
\item the maximal number of simultaneous provers allowed to run in parallel. 
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
240 241
\subsection{Structure of the database file}

242 243 244 245 246 247 248 249 250 251 252 253 254 255
[TO BE COMPLETED LATER]

\section{The \texttt{why3ml} tool}

The \texttt{why3ml} is an additional layer on Why3 library for
generating verification conditions from WhyML programs. This tool and
the syntax of WhyML programs is intentionally left undocumented since
it might evolve significantly in the near future.

For those who want to experiment with it, examples are provided in
\texttt{examples/programs}. The files \texttt{*.mlw} can be loaded in
the GUI.

[TO BE COMPLETED LATER]
MARCHE Claude's avatar
doc  
MARCHE Claude committed
256

257 258
\section{The \texttt{why3bench} tool}

259 260
[TO BE COMPLETED LATER]

MARCHE Claude's avatar
MARCHE Claude committed
261
\section{The \texttt{why.conf} configuration file}
262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
\label{sec:whyconffile}
One can defined more than one configuration file. \texttt{why3config}
and all the others \texttt{why3}'s 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{\$WHY\_CONFIG} if set.
\item the file \texttt{why.conf} or \texttt{.why.conf} in the current
  directory.
\item the file \texttt{\$HOME/.why.conf} or \texttt{\$USERPROFILE/.why.conf}
\end{itemize}
If none of this file exists a built-in default configuration is used
which is saved in a default configuration filename, which is usually
\texttt{\$HOME/.why.conf}.

The configuration file is a human-readable text file, which is
composed by association pairs arranged by sections. Here an example of
a configuration file.

\begin{verbatim}
[main ]
datadir = "/usr/local/share/why3"
libdir = "/usr/local/lib/why3"
loadpath = "/usr/local/share/why3/theories"
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}

A section begin with an header inside square brackets and end at the
next square brackets. Sections can't be nested. The header of a
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.


Inside a section, one key can be associated to an integer (.eg -555),
a boolean (true, false) or a string (.eg "emacs"). One key can appear
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
326

MARCHE Claude's avatar
MARCHE Claude committed
327
\section{Drivers of external provers}
328 329 330 331 332 333 334

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
335 336

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
337
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
338

339 340 341 342
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.

MARCHE Claude's avatar
MARCHE Claude committed
343 344 345
\subsection{Non-splitting transformations}

\begin{description}
346

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

350 351 352
\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
353 354 355
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
356

357 358
\item[eliminate\_if\_fmla] replaces formulas of the form if f1 then f2
  else f3 by an equivalent formula using implications and other
359 360
  connectives. [TO BE COMPLETED LATER]

361
\item[eliminate\_if\_term] replaces terms of the form if formula then
362 363 364
  t2 else t3 by lift it at the level of the formula [TO BE COMPLETED
  LATER]

MARCHE Claude's avatar
MARCHE Claude committed
365
\item[eliminate\_if]
366
  apply both two above transformations
367

368 369
\item[eliminate\_inductive] replaces inductive predicates by
  (incomplete) axiomatic definitions, i.e construction axioms and an
370 371
  inversion axiom [TO BE COMPLETED LATER]

MARCHE Claude's avatar
MARCHE Claude committed
372 373
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
374 375
\item[eliminate\_let]
  apply both two above transformations
376

MARCHE Claude's avatar
MARCHE Claude committed
377 378 379 380 381
\item[eliminate\_mutual\_recursion]
\item[eliminate\_recursion]
\item[encoding\_decorate\_mono]
\item[encoding\_enumeration]
\item[encoding\_simple2]
382

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

MARCHE Claude's avatar
MARCHE Claude committed
386
\item[encoding\_tptp]
387 388
  Encode theories into unsorted logic~\cite{cruanes10}.

MARCHE Claude's avatar
MARCHE Claude committed
389 390 391 392
\item[filter\_trigger]
\item[filter\_trigger\_builtin]
\item[filter\_trigger\_no\_predicate]
\item[hypothesis\_selection]
393 394
  Filter hypothesis of goals~\cite{cruanes10}.

MARCHE Claude's avatar
MARCHE Claude committed
395 396
\item[inline\_all]
\item[inline\_trivial]
397 398 399 400
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
401 402
when each $e_i$ is either a constant or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$ 
403

MARCHE Claude's avatar
MARCHE Claude committed
404
\item[remove\_triggers]
405

MARCHE Claude's avatar
MARCHE Claude committed
406
\item[simplify\_array]
407

408 409 410
\item[simplify\_formula] reduces trivial equalities $t=t$ to True and
  then simplifies propositional structure: removes True, False, ``f
  and f'' to ``f'', etc.
411 412 413

\item[simplify\_recursive\_definition] reduces mutually recursive
  definitions if they are not really mutually recursive, e.g.:
414 415 416 417 418 419 420 421 422 423 424 425
\begin{verbatim}
logic f : ... = .... g ...

with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
logic g : .. = e
logic f : ... = .... g ...
\end{verbatim}
if f does not occur in e

MARCHE Claude's avatar
MARCHE Claude committed
426
\item[simplify\_trivial\_quantification]
427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442
  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
  into 
\begin{verbatim}
P(t)
\end{verbatim}
  More generally, it applies this simplification whenever x=t appear
  in a negative position.
  
MARCHE Claude's avatar
MARCHE Claude committed
443
\item[simplify\_trivial\_quantification\_in\_goal]
444

MARCHE Claude's avatar
MARCHE Claude committed
445
\item[split\_premise]
446

MARCHE Claude's avatar
MARCHE Claude committed
447 448 449 450 451 452 453 454
\end{description}

\subsection{Splitting transformations}

\begin{description}
\item[right\_split]
\item[simplify\_formula\_and\_task]
\item[split\_all]
455 456 457 458

\item[split\_goal] if the goal is a conjunction of goals, returns the
  corresponding set of subgoals.

MARCHE Claude's avatar
MARCHE Claude committed
459 460 461 462 463 464 465 466
\item[split\_goal\_pos\_all]
\item[split\_goal\_pos\_axiom]
\item[split\_goal\_pos\_goal]
\item[split\_goal\_pos\_neg\_all]
\item[split\_goal\_pos\_neg\_axiom]
\item[split\_goal\_pos\_neg\_goal]
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
467

MARCHE Claude's avatar
doc  
MARCHE Claude committed
468 469 470 471 472 473

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