manpages.tex 28 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 When configuration is finished, you can compile \why. \begin{verbatim} make \end{verbatim}  MARCHE Claude committed Jul 07, 2011 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}  Andrei Paskevich committed Dec 20, 2010 82   MARCHE Claude committed Dec 13, 2010 83 84 \subsection{Local use, without installation}  MARCHE Claude committed Jul 02, 2011 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 committed Dec 13, 2010 87 88 89 90 \begin{verbatim} ./configure --enable-local make \end{verbatim}  MARCHE Claude committed Jul 02, 2011 91 The \why executables are then available in the subdirectory \texttt{bin/}.  MARCHE Claude committed Dec 13, 2010 92   MARCHE Claude committed Jul 02, 2011 93 \subsection{Installation of the \why library}  MARCHE Claude committed Dec 16, 2010 94 95 \label{sec:installlib}  MARCHE Claude committed Jul 02, 2011 96 By default, the \why library is not installed. It can be installed using  MARCHE Claude committed Dec 16, 2010 97 98 99 100 \begin{verbatim} make byte opt make install_lib \end{verbatim}  MARCHE Claude committed Dec 16, 2010 101   MARCHE Claude committed Jul 07, 2011 102 \section{Installation of external provers}\label{provers}  MARCHE Claude committed Sep 06, 2010 103   MARCHE Claude committed Jul 02, 2011 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 committed Dec 13, 2010 106 them. There is no need to install these provers before compiling and  Andrei Paskevich committed Jun 30, 2011 107 installing Why.  MARCHE Claude committed Dec 13, 2010 108   MARCHE Claude committed Dec 13, 2010 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 committed Dec 13, 2010 111   MARCHE Claude committed Jul 02, 2011 112 For configuring \why to use the provers, follow instructions given in  MARCHE Claude committed Dec 13, 2010 113 Section~\ref{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 114   MARCHE Claude committed Dec 13, 2010 115 116 \section{The \texttt{why3config} command-line tool} \label{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 117   MARCHE Claude committed Jul 02, 2011 118 \why must be configured to access external provers. Typically, this is done  MARCHE Claude committed Dec 13, 2010 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}  Andrei Paskevich committed Dec 20, 2010 127 of the IDE. This must be redone each time a new prover is installed.  MARCHE Claude committed Dec 13, 2010 128   MARCHE Claude committed Jul 02, 2011 129 The provers which \why attempts to detect are described in  MARCHE Claude committed Dec 13, 2010 130 the readable configuration file \texttt{provers-detection-data.conf}  MARCHE Claude committed Jul 02, 2011 131 of the \why data directory (\eg{}  MARCHE Claude committed Dec 13, 2010 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).  Jean-Christophe Filliâtre committed Feb 17, 2011 137 The result of provers detection is stored in the user's  Andrei Paskevich committed Jul 02, 2011 138 139 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 140 is also human-readable, and advanced users may modify it in order to  Andrei Paskevich committed Jun 30, 2011 141 experiment with different ways of calling provers, \eg{} different  Andrei Paskevich committed Dec 20, 2010 142 versions of the same prover, or with different options.  MARCHE Claude committed Dec 13, 2010 143   Andrei Paskevich committed Dec 20, 2010 144 The provers which are typically looked for are  MARCHE Claude committed Dec 13, 2010 145 \begin{itemize}  MARCHE Claude committed Dec 15, 2010 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 committed Jul 02, 2011 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 committed Dec 15, 2010 156 \item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}  MARCHE Claude committed Dec 13, 2010 157 \end{itemize}  MARCHE Claude committed Dec 13, 2010 158   MARCHE Claude committed Jul 02, 2011 159 \texttt{why3config} also detects the plugins installed in the \why  François Bobot committed Dec 15, 2010 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,  Andrei Paskevich committed Dec 20, 2010 165 \texttt{why3config} will only reset unset variables to default value,  Andrei Paskevich committed Jun 30, 2011 166 but will not try to detect provers.  Jean-Christophe Filliâtre committed Feb 15, 2011 167 The option \texttt{--detect-provers} should be used to force  MARCHE Claude committed Jul 02, 2011 168 \why to detect again the available  Andrei Paskevich committed Dec 20, 2010 169 provers and to replace them in the configuration file. The option  Jean-Christophe Filliâtre committed Feb 15, 2011 170 \texttt{--detect-plugins} will do the same for plugins.  François Bobot committed Dec 15, 2010 171   MARCHE Claude committed Sep 06, 2010 172 \section{The \texttt{why3} command-line tool}  MARCHE Claude committed Dec 15, 2010 173 \label{sec:why3ref}  MARCHE Claude committed Sep 06, 2010 174   MARCHE Claude committed Jul 02, 2011 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  Andrei Paskevich committed Dec 20, 2010 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:  François Bobot committed Dec 15, 2010 182 \begin{enumerate}  Andrei Paskevich committed Dec 20, 2010 183 \item Parse the command line and report errors if needed.  François Bobot committed Dec 15, 2010 184 \item Read the configuration file using the priority defined in  Andrei Paskevich committed Dec 20, 2010 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 committed Jul 02, 2011 189  to obtain a set of \why theories for each file. It uses  Andrei Paskevich committed Dec 20, 2010 190  the filename extension or the \texttt{--format} option to choose  Andrei Paskevich committed Jun 30, 2011 191  among the available parsers. The \texttt{--list-format} option gives  Andrei Paskevich committed Dec 20, 2010 192  the list of registered parsers.  Andrei Paskevich committed Jun 30, 2011 193 \item Extract the selected goals inside each of the selected theories  Andrei Paskevich committed Dec 20, 2010 194 195  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 196  \texttt{-T/--theory} applies to the last file appearing on the  Andrei Paskevich committed Dec 20, 2010 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.  François Bobot committed Dec 15, 2010 201 \item Apply the transformation requested  Andrei Paskevich committed Dec 20, 2010 202  with \texttt{-a/--apply-transform} in their order of appearance on the  François Bobot committed Dec 15, 2010 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}  Andrei Paskevich committed Dec 20, 2010 207  option. \texttt{--list-provers} lists the known provers, i.e.~the ones  François Bobot committed Dec 15, 2010 208  which appear in the configuration file.  Andrei Paskevich committed Dec 20, 2010 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.  François Bobot committed Dec 15, 2010 213 214 \end{enumerate}  Andrei Paskevich committed Dec 20, 2010 215 216 %\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *) %you want to call the provers concurrently. *)  MARCHE Claude committed Dec 17, 2010 217   Andrei Paskevich committed Dec 20, 2010 218 The provers can answer the following output:  François Bobot committed Mar 16, 2011 219 \begin{description}  François Bobot committed Dec 20, 2010 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 committed Mar 16, 2011 225 \end{description}  MARCHE Claude committed Jul 02, 2011 226 % \why can also be *)  MARCHE Claude committed Dec 17, 2010 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} *)  François Bobot committed Dec 15, 2010 233   François Bobot committed Mar 16, 2011 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.  MARCHE Claude committed Dec 16, 2010 244 \section{The \texttt{why3ide} GUI}  MARCHE Claude committed Dec 13, 2010 245 246 \label{sec:ideref}  MARCHE Claude committed Dec 16, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 257 \subsection{Left toolbar actions}  MARCHE Claude committed Dec 13, 2010 258 259  \begin{description}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 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 committed Jul 03, 2011 274  expands it with this definition.  MARCHE Claude committed Dec 15, 2010 275   MARCHE Claude committed Dec 13, 2010 276 277 278 279 280 281 282 283 284 \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 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 committed Dec 15, 2010 290   Andrei Paskevich committed Jun 30, 2011 291 \item[Remove] Removes a proof attempt or a transformation.  MARCHE Claude committed Dec 13, 2010 292   MARCHE Claude committed Jul 03, 2011 293 294 295 \item[Clean] Removes any unsuccessful proof attempt for which there is another successful proof attempt for the same goal  MARCHE Claude committed Sep 23, 2011 296 297 298 \item[Interrupt] Cancels all the proof attempts currently scheduled but not yet started.  MARCHE Claude committed Dec 13, 2010 299 300 301 302 \end{description} \subsection{Menus}  MARCHE Claude committed Dec 20, 2010 303 \paragraph{Menu \textsf{File}}  MARCHE Claude committed Dec 13, 2010 304 \begin{description}  MARCHE Claude committed Dec 20, 2010 305 \item[Add File] adds a file in the GUI  MARCHE Claude committed Jul 03, 2011 306 %\item[Detect provers] runs provers auto-detection  MARCHE Claude committed Dec 20, 2010 307 \item[Preferences] opens a window for modifying preferred  MARCHE Claude committed Jul 04, 2011 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.  MARCHE Claude committed Dec 20, 2010 311 \item[Quit] exits the GUI  MARCHE Claude committed Dec 13, 2010 312 \end{description}  MARCHE Claude committed Dec 13, 2010 313   MARCHE Claude committed Dec 20, 2010 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 committed Jul 03, 2011 319 320 % \item[Hide proved goals] completely hides the proved rows of the tree % view [EXPERIMENTAL]  MARCHE Claude committed Dec 20, 2010 321 322 323 \end{description} \paragraph{Menu \textsf{Tools}}  MARCHE Claude committed Jul 05, 2011 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}  MARCHE Claude committed Dec 20, 2010 329 330 331 332  \paragraph{Menu \textsf{Help}} A very short online help, and some information about this software.  MARCHE Claude committed Dec 13, 2010 333 334 \subsection{Preferences}  MARCHE Claude committed Dec 15, 2010 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  Andrei Paskevich committed Jun 30, 2011 341 \item the maximal number of simultaneous provers allowed to run in parallel.  MARCHE Claude committed Jul 04, 2011 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 committed Dec 15, 2010 349 350 \end{itemize}  MARCHE Claude committed Dec 13, 2010 351 352 \subsection{Structure of the database file}  MARCHE Claude committed Jul 04, 2011 353 354 355 356 357 358 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 359 360 361  \section{The \texttt{why3ml} tool}  MARCHE Claude committed Jul 02, 2011 362 363 \texttt{why3ml} is an additional layer on \why library for generating verification conditions from \whyml programs.  Jean-Christophe Filliâtre committed May 31, 2011 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 committed Jul 02, 2011 366 input files containing \whyml modules (see chapter~\ref{chap:whyml}  Jean-Christophe Filliâtre committed May 31, 2011 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 committed Sep 06, 2010 376   François Bobot committed Dec 15, 2010 377 \section{The \texttt{why3bench} tool}  MARCHE Claude committed Dec 20, 2010 378   MARCHE Claude committed Jul 02, 2011 379 The \texttt{why3bench} tool adds a scheduler on top of the \why  François Bobot committed Dec 20, 2010 380 library. \texttt{why3bench} is designed to compare various components  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 385 \begin{itemize}  MARCHE Claude committed Dec 20, 2010 386 \item csv: the simpler and more informative format, the results are  François Bobot committed Dec 20, 2010 387  represented in an array, the rows corresponds to the  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 395 \end{itemize}  François Bobot committed Dec 15, 2010 396   MARCHE Claude committed Dec 20, 2010 397 The compared components can be defined in an \emph{rc-file},  MARCHE Claude committed Dec 20, 2010 398 \texttt{examples/programs/\ prgbench.rc} is such an example. More  MARCHE Claude committed Dec 20, 2010 399 generally a bench configuration file:  François Bobot committed Dec 20, 2010 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 = "..."  Andrei Paskevich committed Jul 02, 2011 418  loadpath = "..." #added to the one in why3.conf  François Bobot committed Dec 20, 2010 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}  Jean-Christophe Filliâtre committed Feb 17, 2011 438 Such a file can define three families \texttt{tools,probs,bench}. The  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 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  Jean-Christophe Filliâtre committed Feb 17, 2011 445 \texttt{tools} can be used to compare different axiomatizations.  François Bobot committed Dec 20, 2010 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}  MARCHE Claude committed Dec 17, 2010 452   MARCHE Claude committed Jul 03, 2011 453 \section{The \texttt{why3replayer} tool}  MARCHE Claude committed Jul 04, 2011 454 \label{sec:why3replayer}  MARCHE Claude committed Jul 03, 2011 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  MARCHE Claude committed Jul 04, 2011 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 committed Jul 03, 2011 461   MARCHE Claude committed Sep 14, 2011 462 The tool is invoked in a terminal or a script using  MARCHE Claude committed Jul 03, 2011 463 464 465 466 467 468 \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  MARCHE Claude committed Jul 04, 2011 469 the new run are shown.  MARCHE Claude committed Jul 03, 2011 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 committed Sep 14, 2011 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 committed Jul 03, 2011 484 485  \paragraph{Exit code and options}  MARCHE Claude committed Sep 14, 2011 486   MARCHE Claude committed Jul 03, 2011 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 committed Sep 14, 2011 491 492 \item option \texttt{-I \textsl{}}: add \textsl{} to the loadpath \item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.  MARCHE Claude committed Oct 11, 2011 493 494 495 496 497 498 499 \item option \texttt{-latex \textsl{}}: 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{}}. \item option \texttt{-latex2 \textsl{}}: alternate version of LaTeX output, with a different layout of the tables. % \item option \texttt{-html \textsl{}}: produce a summary of % the replay in HTML syntax.  MARCHE Claude committed Jul 03, 2011 500 501 \end{itemize}  MARCHE Claude committed Oct 11, 2011 502 \paragraph{Customizing LaTeX output}  Asma Tafat-Bouzid committed Oct 11, 2011 503   MARCHE Claude committed Oct 11, 2011 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 committed Oct 11, 2011 507 \begin{itemize}  MARCHE Claude committed Oct 11, 2011 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 committed Oct 11, 2011 527 528 529   Asma Tafat-Bouzid committed Oct 11, 2011 530   Andrei Paskevich committed Jul 02, 2011 531 \section{The \texttt{why3.conf} configuration file}  François Bobot committed Dec 15, 2010 532 533 534 \label{sec:whyconffile}  MARCHE Claude committed Oct 11, 2011 535 \begin{figure}[t]  François Bobot committed Dec 15, 2010 536 537 538 \begin{verbatim} [main ] loadpath = "/usr/local/share/why3/theories"  Jean-Christophe Filliâtre committed Feb 17, 2011 539 magic = 2  François Bobot committed Dec 15, 2010 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}  MARCHE Claude committed Oct 11, 2011 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.  François Bobot committed Dec 15, 2010 588   Jean-Christophe Filliâtre committed Feb 17, 2011 589 590 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 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.  Jean-Christophe Filliâtre committed Feb 17, 2011 596 Inside a section, one key can be associated with an integer (.eg -555),  MARCHE Claude committed Dec 17, 2010 597 a boolean (true, false) or a string (\eg{} "emacs"). One key can appear  François Bobot committed Dec 15, 2010 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 committed Sep 06, 2010 600   Jean-Christophe Filliâtre committed Feb 17, 2011 601 \section{Drivers of External Provers}  Andrei Paskevich committed Dec 20, 2010 602 \label{sec:drivers}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 610 611  \section{Transformations}  MARCHE Claude committed Dec 15, 2010 612 \label{sec:transformations}  MARCHE Claude committed Sep 08, 2010 613   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 20, 2010 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 committed Sep 08, 2010 624 625 626 \subsection{Non-splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 627   MARCHE Claude committed Sep 08, 2010 628 629 \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr}  MARCHE Claude committed Dec 17, 2010 630   MARCHE Claude committed Sep 09, 2010 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 committed Sep 08, 2010 633 \item[eliminate\_definition\_func]  MARCHE Claude committed Dec 17, 2010 634  Replaces all function definitions with axioms.  MARCHE Claude committed Sep 08, 2010 635 \item[eliminate\_definition\_pred]  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 643   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 647   MARCHE Claude committed Dec 17, 2010 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  Andrei Paskevich committed Jun 30, 2011 650  connectives.  MARCHE Claude committed Dec 17, 2010 651   MARCHE Claude committed Sep 08, 2010 652 \item[eliminate\_if]  MARCHE Claude committed Dec 17, 2010 653  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 654   MARCHE Claude committed Sep 09, 2010 655 \item[eliminate\_inductive] replaces inductive predicates by  MARCHE Claude committed Dec 17, 2010 656 657  (incomplete) axiomatic definitions, i.e. construction axioms and an inversion axiom.  MARCHE Claude committed Dec 17, 2010 658   MARCHE Claude committed Sep 08, 2010 659 \item[eliminate\_let\_fmla]  MARCHE Claude committed Dec 17, 2010 660 661  Eliminates \texttt{let} by substitution, at the predicate level.  MARCHE Claude committed Sep 08, 2010 662 \item[eliminate\_let\_term]  MARCHE Claude committed Dec 17, 2010 663 664  Eliminates \texttt{let} by substitution, at the term level.  MARCHE Claude committed Sep 09, 2010 665 \item[eliminate\_let]  MARCHE Claude committed Dec 17, 2010 666  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 667   MARCHE Claude committed Dec 17, 2010 668 669 670 % \item[encoding\_decorate\_mono] % \item[encoding\_enumeration]  MARCHE Claude committed Dec 17, 2010 671   MARCHE Claude committed Sep 08, 2010 672 \item[encoding\_smt]  MARCHE Claude committed Dec 17, 2010 673 674  Encode polymorphic types into monomorphic type~\cite{conchon08smt}.  MARCHE Claude committed Sep 08, 2010 675 \item[encoding\_tptp]  MARCHE Claude committed Dec 17, 2010 676  Encode theories into unsorted logic. %~\cite{cruanes10}.  MARCHE Claude committed Dec 17, 2010 677   MARCHE Claude committed Dec 17, 2010 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}. *)  MARCHE Claude committed Dec 17, 2010 686   MARCHE Claude committed Sep 08, 2010 687 \item[inline\_all]  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 693 \item[inline\_trivial]  MARCHE Claude committed Sep 09, 2010 694  removes definitions of the form  MARCHE Claude committed Dec 17, 2010 695   MARCHE Claude committed Sep 09, 2010 696 \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 697 698 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 699 \end{verbatim}  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Sep 09, 2010 705   MARCHE Claude committed Dec 17, 2010 706 707 % \item[remove\_triggers] *) % removes the triggers in all quantifications. *)  MARCHE Claude committed Dec 17, 2010 708   MARCHE Claude committed Dec 17, 2010 709 710 \item[simplify\_array] Automatically rewrites the task using the lemma \verb|Select_eq| of theory \verb|array.Array|.  MARCHE Claude committed Dec 17, 2010 711   MARCHE Claude committed Dec 17, 2010 712 713 \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 714  and f'' to f'', etc.  MARCHE Claude committed Dec 17, 2010 715 716 717  \item[simplify\_recursive\_definition] reduces mutually recursive definitions if they are not really mutually recursive, e.g.:  MARCHE Claude committed Sep 09, 2010 718 \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 719 function f : ... = .... g ...  MARCHE Claude committed Sep 09, 2010 720 721 722 723 724  with g : .. = e \end{verbatim} becomes \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 725 726 function g : .. = e function f : ... = .... g ...  MARCHE Claude committed Sep 09, 2010 727 728 729 \end{verbatim} if f does not occur in e  MARCHE Claude committed Sep 08, 2010 730 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 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  Andrei Paskevich committed Jun 30, 2011 740  into  MARCHE Claude committed Sep 09, 2010 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.  Andrei Paskevich committed Jun 30, 2011 746   MARCHE Claude committed Sep 08, 2010 747 \item[simplify\_trivial\_quantification\_in\_goal]  MARCHE Claude committed Dec 17, 2010 748  same as above but applies only in the goal.  MARCHE Claude committed Dec 17, 2010 749   MARCHE Claude committed Sep 08, 2010 750 \item[split\_premise]  MARCHE Claude committed Dec 17, 2010 751  splits conjunctive premises.  MARCHE Claude committed Dec 17, 2010 752   MARCHE Claude committed Sep 08, 2010 753 754 755 756 757 \end{description} \subsection{Splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 769 \item[split\_all]  MARCHE Claude committed Dec 17, 2010 770  composition of \texttt{split\_premise} and \texttt{split\_goal}.  MARCHE Claude committed Dec 17, 2010 771 772  \item[split\_goal] if the goal is a conjunction of goals, returns the  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 779 780 \end{description}  MARCHE Claude committed Sep 06, 2010 781   MARCHE Claude committed Sep 06, 2010 782 783 784 785 786 787  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: