manpages.tex 25.2 KB
 MARCHE Claude committed Jul 02, 2011 1 \chapter{Reference manuals for the \why tools}  MARCHE Claude committed Sep 08, 2010 2 \label{chap:manpages}  MARCHE Claude committed Sep 06, 2010 3 4  \section{Compilation, Installation}  MARCHE Claude committed Dec 13, 2010 5 \label{sec:install}  MARCHE Claude committed Sep 06, 2010 6   MARCHE Claude committed Jul 02, 2011 7 Compilation of \why must start with a configuration phase which is run as  MARCHE Claude committed Sep 07, 2010 8 9 10 \begin{verbatim} ./configure \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 11 This analyzes your current configuration and checks if requirements hold.  MARCHE Claude committed Sep 07, 2010 12 13 Compilation requires: \begin{itemize}  MARCHE Claude committed Dec 08, 2010 14 15 \item The Objective Caml compiler, version 3.10 or higher. It is available as a binary package for most Unix distributions. For  Andrei Paskevich committed Dec 20, 2010 16  Debian-based Linux distributions, you can install the packages  MARCHE Claude committed Sep 07, 2010 17 18 19 \begin{verbatim} ocaml ocaml-native-compilers \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 20 It is also installable from sources, downloadable from the site  MARCHE Claude committed Sep 07, 2010 21 \url{http://caml.inria.fr/ocaml/}  MARCHE Claude committed Dec 13, 2010 22 \end{itemize}  MARCHE Claude committed Sep 07, 2010 23   MARCHE Claude committed Jul 02, 2011 24 For some tools, additional OCaml libraries are needed:  MARCHE Claude committed Dec 13, 2010 25 \begin{itemize}  MARCHE Claude committed Jul 02, 2011 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 committed Sep 07, 2010 29 30 31 \begin{verbatim} liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 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 committed Sep 07, 2010 34   MARCHE Claude committed Jul 02, 2011 35 \item For \texttt{why3bench}: The OCaml bindings of the sqlite3 library.  Andrei Paskevich committed Dec 20, 2010 36 For Debian-based Linux distributions, you can install the package  MARCHE Claude committed Dec 13, 2010 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 committed Sep 07, 2010 42 43 \end{itemize}  Andrei Paskevich committed Dec 20, 2010 44 45 46 47 48 When configuration is finished, you can compile \why. \begin{verbatim} make \end{verbatim}  MARCHE Claude committed Dec 13, 2010 49 50 \subsection{Local use, without installation}  MARCHE Claude committed Jul 02, 2011 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 committed Dec 13, 2010 53 54 55 56 \begin{verbatim} ./configure --enable-local make \end{verbatim}  MARCHE Claude committed Jul 02, 2011 57 The \why executables are then available in the subdirectory \texttt{bin/}.  MARCHE Claude committed Dec 13, 2010 58   MARCHE Claude committed Jul 02, 2011 59 \subsection{Installation of the \why library}  MARCHE Claude committed Dec 16, 2010 60 61 \label{sec:installlib}  MARCHE Claude committed Jul 02, 2011 62 By default, the \why library is not installed. It can be installed using  MARCHE Claude committed Dec 16, 2010 63 64 65 66 \begin{verbatim} make byte opt make install_lib \end{verbatim}  MARCHE Claude committed Dec 16, 2010 67   MARCHE Claude committed Sep 06, 2010 68 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 69   MARCHE Claude committed Jul 02, 2011 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 committed Dec 13, 2010 72 them. There is no need to install these provers before compiling and  Andrei Paskevich committed Jun 30, 2011 73 installing Why.  MARCHE Claude committed Dec 13, 2010 74   MARCHE Claude committed Dec 13, 2010 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 committed Dec 13, 2010 77   MARCHE Claude committed Jul 02, 2011 78 For configuring \why to use the provers, follow instructions given in  MARCHE Claude committed Dec 13, 2010 79 Section~\ref{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 80   MARCHE Claude committed Dec 13, 2010 81 82 \section{The \texttt{why3config} command-line tool} \label{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 83   MARCHE Claude committed Jul 02, 2011 84 \why must be configured to access external provers. Typically, this is done  MARCHE Claude committed Dec 13, 2010 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}  Andrei Paskevich committed Dec 20, 2010 93 of the IDE. This must be redone each time a new prover is installed.  MARCHE Claude committed Dec 13, 2010 94   MARCHE Claude committed Jul 02, 2011 95 The provers which \why attempts to detect are described in  MARCHE Claude committed Dec 13, 2010 96 the readable configuration file \texttt{provers-detection-data.conf}  MARCHE Claude committed Jul 02, 2011 97 of the \why data directory (\eg{}  MARCHE Claude committed Dec 13, 2010 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).  Jean-Christophe Filliâtre committed Feb 17, 2011 103 The result of provers detection is stored in the user's  Andrei Paskevich committed Jul 02, 2011 104 105 configuration file (\verb+~/.why3.conf+ or, in the case of local installation, \verb+why3.conf+ in Why3 sources top directory). This file  Jean-Christophe Filliâtre committed Feb 17, 2011 106 is also human-readable, and advanced users may modify it in order to  Andrei Paskevich committed Jun 30, 2011 107 experiment with different ways of calling provers, \eg{} different  Andrei Paskevich committed Dec 20, 2010 108 versions of the same prover, or with different options.  MARCHE Claude committed Dec 13, 2010 109   Andrei Paskevich committed Dec 20, 2010 110 The provers which are typically looked for are  MARCHE Claude committed Dec 13, 2010 111 \begin{itemize}  MARCHE Claude committed Dec 15, 2010 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 committed Jul 02, 2011 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 committed Dec 15, 2010 122 \item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}  MARCHE Claude committed Dec 13, 2010 123 \end{itemize}  MARCHE Claude committed Dec 13, 2010 124   MARCHE Claude committed Jul 02, 2011 125 \texttt{why3config} also detects the plugins installed in the \why  François Bobot committed Dec 15, 2010 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,  Andrei Paskevich committed Dec 20, 2010 131 \texttt{why3config} will only reset unset variables to default value,  Andrei Paskevich committed Jun 30, 2011 132 but will not try to detect provers.  Jean-Christophe Filliâtre committed Feb 15, 2011 133 The option \texttt{--detect-provers} should be used to force  MARCHE Claude committed Jul 02, 2011 134 \why to detect again the available  Andrei Paskevich committed Dec 20, 2010 135 provers and to replace them in the configuration file. The option  Jean-Christophe Filliâtre committed Feb 15, 2011 136 \texttt{--detect-plugins} will do the same for plugins.  François Bobot committed Dec 15, 2010 137   MARCHE Claude committed Sep 06, 2010 138 \section{The \texttt{why3} command-line tool}  MARCHE Claude committed Dec 15, 2010 139 \label{sec:why3ref}  MARCHE Claude committed Sep 06, 2010 140   MARCHE Claude committed Jul 02, 2011 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  Andrei Paskevich committed Dec 20, 2010 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:  François Bobot committed Dec 15, 2010 148 \begin{enumerate}  Andrei Paskevich committed Dec 20, 2010 149 \item Parse the command line and report errors if needed.  François Bobot committed Dec 15, 2010 150 \item Read the configuration file using the priority defined in  Andrei Paskevich committed Dec 20, 2010 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 committed Jul 02, 2011 155  to obtain a set of \why theories for each file. It uses  Andrei Paskevich committed Dec 20, 2010 156  the filename extension or the \texttt{--format} option to choose  Andrei Paskevich committed Jun 30, 2011 157  among the available parsers. The \texttt{--list-format} option gives  Andrei Paskevich committed Dec 20, 2010 158  the list of registered parsers.  Andrei Paskevich committed Jun 30, 2011 159 \item Extract the selected goals inside each of the selected theories  Andrei Paskevich committed Dec 20, 2010 160 161  into tasks. The goals and theories are selected using the options \texttt{-G/--goal} and \texttt{-T/--theory}. The option  François Bobot committed Dec 15, 2010 162  \texttt{-T/--theory} applies to the last file appearing on the  Andrei Paskevich committed Dec 20, 2010 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.  François Bobot committed Dec 15, 2010 167 \item Apply the transformation requested  Andrei Paskevich committed Dec 20, 2010 168  with \texttt{-a/--apply-transform} in their order of appearance on the  François Bobot committed Dec 15, 2010 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}  Andrei Paskevich committed Dec 20, 2010 173  option. \texttt{--list-provers} lists the known provers, i.e.~the ones  François Bobot committed Dec 15, 2010 174  which appear in the configuration file.  Andrei Paskevich committed Dec 20, 2010 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.  François Bobot committed Dec 15, 2010 179 180 \end{enumerate}  Andrei Paskevich committed Dec 20, 2010 181 182 %\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *) %you want to call the provers concurrently. *)  MARCHE Claude committed Dec 17, 2010 183   Andrei Paskevich committed Dec 20, 2010 184 The provers can answer the following output:  François Bobot committed Mar 16, 2011 185 \begin{description}  François Bobot committed Dec 20, 2010 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 committed Mar 16, 2011 191 \end{description}  MARCHE Claude committed Jul 02, 2011 192 % \why can also be *)  MARCHE Claude committed Dec 17, 2010 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} *)  François Bobot committed Dec 15, 2010 199   François Bobot committed Mar 16, 2011 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.  MARCHE Claude committed Dec 16, 2010 210 \section{The \texttt{why3ide} GUI}  MARCHE Claude committed Dec 13, 2010 211 212 \label{sec:ideref}  MARCHE Claude committed Dec 16, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 223 \subsection{Left toolbar actions}  MARCHE Claude committed Dec 13, 2010 224 225  \begin{description}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 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 committed Jul 03, 2011 240  expands it with this definition.  MARCHE Claude committed Dec 15, 2010 241   MARCHE Claude committed Dec 13, 2010 242 243 244 245 246 247 248 249 250 \item 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 committed Jul 03, 2011 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 committed Dec 15, 2010 256   Andrei Paskevich committed Jun 30, 2011 257 \item[Remove] Removes a proof attempt or a transformation.  MARCHE Claude committed Dec 13, 2010 258   MARCHE Claude committed Jul 03, 2011 259 260 261 \item[Clean] Removes any unsuccessful proof attempt for which there is another successful proof attempt for the same goal  MARCHE Claude committed Dec 13, 2010 262 263 264 265 \end{description} \subsection{Menus}  MARCHE Claude committed Dec 20, 2010 266 \paragraph{Menu \textsf{File}}  MARCHE Claude committed Dec 13, 2010 267 \begin{description}  MARCHE Claude committed Dec 20, 2010 268 \item[Add File] adds a file in the GUI  MARCHE Claude committed Jul 03, 2011 269 %\item[Detect provers] runs provers auto-detection  MARCHE Claude committed Dec 20, 2010 270 \item[Preferences] opens a window for modifying preferred  MARCHE Claude committed Jul 04, 2011 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.  MARCHE Claude committed Dec 20, 2010 274 \item[Quit] exits the GUI  MARCHE Claude committed Dec 13, 2010 275 \end{description}  MARCHE Claude committed Dec 13, 2010 276   MARCHE Claude committed Dec 20, 2010 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 committed Jul 03, 2011 282 283 % \item[Hide proved goals] completely hides the proved rows of the tree % view [EXPERIMENTAL]  MARCHE Claude committed Dec 20, 2010 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 committed Dec 13, 2010 292 293 \subsection{Preferences}  MARCHE Claude committed Dec 15, 2010 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  Andrei Paskevich committed Jun 30, 2011 300 \item the maximal number of simultaneous provers allowed to run in parallel.  MARCHE Claude committed Jul 04, 2011 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 committed Dec 15, 2010 308 309 \end{itemize}  MARCHE Claude committed Dec 13, 2010 310 311 \subsection{Structure of the database file}  MARCHE Claude committed Jul 04, 2011 312 313 314 315 316 317 The session state is stored in an XML file named \texttt{\textsl{}/why3session.xml}, where \texttt{\textsl{}} 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}  MARCHE Claude committed Dec 17, 2010 318 319 320  \section{The \texttt{why3ml} tool}  MARCHE Claude committed Jul 02, 2011 321 322 \texttt{why3ml} is an additional layer on \why library for generating verification conditions from \whyml programs.  Jean-Christophe Filliâtre committed May 31, 2011 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 committed Jul 02, 2011 325 input files containing \whyml modules (see chapter~\ref{chap:whyml}  Jean-Christophe Filliâtre committed May 31, 2011 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 committed Sep 06, 2010 335   François Bobot committed Dec 15, 2010 336 \section{The \texttt{why3bench} tool}  MARCHE Claude committed Dec 20, 2010 337   MARCHE Claude committed Jul 02, 2011 338 The \texttt{why3bench} tool adds a scheduler on top of the \why  François Bobot committed Dec 20, 2010 339 library. \texttt{why3bench} is designed to compare various components  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 344 \begin{itemize}  MARCHE Claude committed Dec 20, 2010 345 \item csv: the simpler and more informative format, the results are  François Bobot committed Dec 20, 2010 346  represented in an array, the rows corresponds to the  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 354 \end{itemize}  François Bobot committed Dec 15, 2010 355   MARCHE Claude committed Dec 20, 2010 356 The compared components can be defined in an \emph{rc-file},  MARCHE Claude committed Dec 20, 2010 357 \texttt{examples/programs/\ prgbench.rc} is such an example. More  MARCHE Claude committed Dec 20, 2010 358 generally a bench configuration file:  François Bobot committed Dec 20, 2010 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 = "..."  Andrei Paskevich committed Jul 02, 2011 377  loadpath = "..." #added to the one in why3.conf  François Bobot committed Dec 20, 2010 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}  Jean-Christophe Filliâtre committed Feb 17, 2011 397 Such a file can define three families \texttt{tools,probs,bench}. The  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 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  Jean-Christophe Filliâtre committed Feb 17, 2011 404 \texttt{tools} can be used to compare different axiomatizations.  François Bobot committed Dec 20, 2010 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}  MARCHE Claude committed Dec 17, 2010 411   MARCHE Claude committed Jul 03, 2011 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] } \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{}}: suppresses the output of the final tree view \end{itemize}  Andrei Paskevich committed Jul 02, 2011 463 \section{The \texttt{why3.conf} configuration file}  François Bobot committed Dec 15, 2010 464 \label{sec:whyconffile}  Jean-Christophe Filliâtre committed Feb 17, 2011 465 466 One can use a custom configuration file. \texttt{why3config} and other \texttt{why3} tools use priorities for which  François Bobot committed Dec 15, 2010 467 468 user's configuration file to consider: \begin{itemize}  Jean-Christophe Filliâtre committed Feb 17, 2011 469 \item the file specified by the \texttt{-C} or \texttt{-{}-config} options,  François Bobot committed Dec 15, 2010 470 \item the file specified by the environment variable  Jean-Christophe Filliâtre committed Feb 17, 2011 471  \texttt{WHY3CONFIG} if set.  Andrei Paskevich committed Jul 02, 2011 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.  François Bobot committed Dec 15, 2010 475 \end{itemize}  Jean-Christophe Filliâtre committed Feb 17, 2011 476 If none of these files exists, a built-in default configuration is used.  François Bobot committed Dec 15, 2010 477   Jean-Christophe Filliâtre committed Feb 17, 2011 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.  François Bobot committed Dec 15, 2010 481 482 483 484  \begin{verbatim} [main ] loadpath = "/usr/local/share/why3/theories"  Jean-Christophe Filliâtre committed Feb 17, 2011 485 magic = 2  François Bobot committed Dec 15, 2010 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}  Jean-Christophe Filliâtre committed Feb 17, 2011 513 514 A section begins with a header inside square brackets and ends at the beginning of the next section. The header of a  François Bobot committed Dec 15, 2010 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.  Jean-Christophe Filliâtre committed Feb 17, 2011 520 Inside a section, one key can be associated with an integer (.eg -555),  MARCHE Claude committed Dec 17, 2010 521 a boolean (true, false) or a string (\eg{} "emacs"). One key can appear  François Bobot committed Dec 15, 2010 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 committed Sep 06, 2010 524   Jean-Christophe Filliâtre committed Feb 17, 2011 525 \section{Drivers of External Provers}  Andrei Paskevich committed Dec 20, 2010 526 \label{sec:drivers}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 534 535  \section{Transformations}  MARCHE Claude committed Dec 15, 2010 536 \label{sec:transformations}  MARCHE Claude committed Sep 08, 2010 537   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 20, 2010 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 committed Sep 08, 2010 548 549 550 \subsection{Non-splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 551   MARCHE Claude committed Sep 08, 2010 552 553 \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr}  MARCHE Claude committed Dec 17, 2010 554   MARCHE Claude committed Sep 09, 2010 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 committed Sep 08, 2010 557 \item[eliminate\_definition\_func]  MARCHE Claude committed Dec 17, 2010 558  Replaces all function definitions with axioms.  MARCHE Claude committed Sep 08, 2010 559 \item[eliminate\_definition\_pred]  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 567   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 571   MARCHE Claude committed Dec 17, 2010 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  Andrei Paskevich committed Jun 30, 2011 574  connectives.  MARCHE Claude committed Dec 17, 2010 575   MARCHE Claude committed Sep 08, 2010 576 \item[eliminate\_if]  MARCHE Claude committed Dec 17, 2010 577  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 578   MARCHE Claude committed Sep 09, 2010 579 \item[eliminate\_inductive] replaces inductive predicates by  MARCHE Claude committed Dec 17, 2010 580 581  (incomplete) axiomatic definitions, i.e. construction axioms and an inversion axiom.  MARCHE Claude committed Dec 17, 2010 582   MARCHE Claude committed Sep 08, 2010 583 \item[eliminate\_let\_fmla]  MARCHE Claude committed Dec 17, 2010 584 585  Eliminates \texttt{let} by substitution, at the predicate level.  MARCHE Claude committed Sep 08, 2010 586 \item[eliminate\_let\_term]  MARCHE Claude committed Dec 17, 2010 587 588  Eliminates \texttt{let} by substitution, at the term level.  MARCHE Claude committed Sep 09, 2010 589 \item[eliminate\_let]  MARCHE Claude committed Dec 17, 2010 590  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 591   MARCHE Claude committed Dec 17, 2010 592 593 594 % \item[encoding\_decorate\_mono] % \item[encoding\_enumeration]  MARCHE Claude committed Dec 17, 2010 595   MARCHE Claude committed Sep 08, 2010 596 \item[encoding\_smt]  MARCHE Claude committed Dec 17, 2010 597 598  Encode polymorphic types into monomorphic type~\cite{conchon08smt}.  MARCHE Claude committed Sep 08, 2010 599 \item[encoding\_tptp]  MARCHE Claude committed Dec 17, 2010 600  Encode theories into unsorted logic. %~\cite{cruanes10}.  MARCHE Claude committed Dec 17, 2010 601   MARCHE Claude committed Dec 17, 2010 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}. *)  MARCHE Claude committed Dec 17, 2010 610   MARCHE Claude committed Sep 08, 2010 611 \item[inline\_all]  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 617 \item[inline\_trivial]  MARCHE Claude committed Sep 09, 2010 618  removes definitions of the form  MARCHE Claude committed Dec 17, 2010 619   MARCHE Claude committed Sep 09, 2010 620 \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 621 622 function f x_1 .. x_n = (g e_1 .. e_k) predicate p x_1 .. x_n = (q e_1 .. e_k)  MARCHE Claude committed Sep 09, 2010 623 \end{verbatim}  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Sep 09, 2010 629   MARCHE Claude committed Dec 17, 2010 630 631 % \item[remove\_triggers] *) % removes the triggers in all quantifications. *)  MARCHE Claude committed Dec 17, 2010 632   MARCHE Claude committed Dec 17, 2010 633 634 \item[simplify\_array] Automatically rewrites the task using the lemma \verb|Select_eq| of theory \verb|array.Array|.  MARCHE Claude committed Dec 17, 2010 635   MARCHE Claude committed Dec 17, 2010 636 637 \item[simplify\_formula] reduces trivial equalities$t=t\$ to true and then simplifies propositional structure: removes true, false, f  MARCHE Claude committed Sep 09, 2010 638  and f'' to f'', etc.  MARCHE Claude committed Dec 17, 2010 639 640 641  \item[simplify\_recursive\_definition] reduces mutually recursive definitions if they are not really mutually recursive, e.g.:  MARCHE Claude committed Sep 09, 2010 642 \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 643 function f : ... = .... g ...  MARCHE Claude committed Sep 09, 2010 644 645 646 647 648  with g : .. = e \end{verbatim} becomes \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 649 650 function g : .. = e function f : ... = .... g ...  MARCHE Claude committed Sep 09, 2010 651 652 653 \end{verbatim} if f does not occur in e  MARCHE Claude committed Sep 08, 2010 654 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 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  Andrei Paskevich committed Jun 30, 2011 664  into  MARCHE Claude committed Sep 09, 2010 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.  Andrei Paskevich committed Jun 30, 2011 670   MARCHE Claude committed Sep 08, 2010 671 \item[simplify\_trivial\_quantification\_in\_goal]  MARCHE Claude committed Dec 17, 2010 672  same as above but applies only in the goal.  MARCHE Claude committed Dec 17, 2010 673   MARCHE Claude committed Sep 08, 2010 674 \item[split\_premise]  MARCHE Claude committed Dec 17, 2010 675  splits conjunctive premises.  MARCHE Claude committed Dec 17, 2010 676   MARCHE Claude committed Sep 08, 2010 677 678 679 680 681 \end{description} \subsection{Splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 693 \item[split\_all]  MARCHE Claude committed Dec 17, 2010 694  composition of \texttt{split\_premise} and \texttt{split\_goal}.  MARCHE Claude committed Dec 17, 2010 695 696  \item[split\_goal] if the goal is a conjunction of goals, returns the  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 703 704 \end{description}  MARCHE Claude committed Sep 06, 2010 705   MARCHE Claude committed Sep 06, 2010 706 707 708 709 710 711  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: