Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. 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 7.83 KB
 MARCHE Claude committed Sep 06, 2010 1 \chapter{Reference manuals for the Why3 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 Sep 07, 2010 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 committed Dec 08, 2010 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 committed Sep 07, 2010 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 committed Dec 13, 2010 22 \end{itemize}  MARCHE Claude committed Sep 07, 2010 23   MARCHE Claude committed Dec 13, 2010 24 25 For the IDE, additional Ocaml libraries are needed: \begin{itemize}  MARCHE Claude committed Sep 07, 2010 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 committed Dec 13, 2010 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 committed Sep 07, 2010 40 41 \end{itemize}  MARCHE Claude committed Dec 13, 2010 42 43 \subsection{Local use, without installation}  MARCHE Claude committed Dec 13, 2010 44 It is not mandatory to install Why3 to use it. Local use is obtained via  MARCHE Claude committed Dec 13, 2010 45 46 47 48 \begin{verbatim} ./configure --enable-local make \end{verbatim}  MARCHE Claude committed Dec 13, 2010 49 The Why3 executables are then available in subdirectory \texttt{bin/}.  MARCHE Claude committed Dec 13, 2010 50   MARCHE Claude committed Sep 06, 2010 51 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 52   MARCHE Claude committed Dec 13, 2010 53 54 55 56 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 committed Dec 13, 2010 57   MARCHE Claude committed Dec 13, 2010 58 59 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 60   MARCHE Claude committed Dec 13, 2010 61 62 For configuring Why3 to use the provers, follow intructions given in Section~\ref{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 63   MARCHE Claude committed Dec 13, 2010 64 65 \section{The \texttt{why3config} command-line tool} \label{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 66   MARCHE Claude committed Dec 13, 2010 67 68 69 70 71 72 73 74 75 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 103 104 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} \item Alt-Ergo~\cite{conchon08smt,ergo}: \url{} \item CVC3~\cite{BarTin-CAV-07}: \url{} \item Coq~\cite{CoqArt}: \url{} \item Eprover~: \url{} \item Gappa~\cite{melquiond08rnc}: \url{} \item Simplify~\cite{simplify05}: \url{} \item Spass~: \url{} \item veriT~: \url{} \item Yices~\cite{DM06}: \url{} \item Z3~\cite{z3}: \url{} \end{itemize}  MARCHE Claude committed Dec 13, 2010 105   MARCHE Claude committed Sep 06, 2010 106 107 108 109 110 \section{The \texttt{why3} command-line tool} \section{The \texttt{why3ml} tool} \section{The \texttt{why3ide} tool}  MARCHE Claude committed Dec 13, 2010 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 \label{sec:ideref} \subsection{Command-line options} \begin{description} \item[-I] $d$: adds $d$ in the load path, to search for theories. \end{description} \subsection{Left toolbar} \begin{description} \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). \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. \item[Split] This splits the current goal into subgoals if it is a conjunction of two or more goals. \end{description} \subsection{Menus} \begin{description} \item[File/Detect provers] \end{description}  MARCHE Claude committed Dec 13, 2010 146   MARCHE Claude committed Dec 13, 2010 147 148 149 150 \subsection{Preferences} \subsection{Structure of the database file}  MARCHE Claude committed Dec 13, 2010 151 [TODO]  MARCHE Claude committed Sep 06, 2010 152   MARCHE Claude committed Sep 06, 2010 153 154 \section{The \texttt{why.conf} configuration file}  MARCHE Claude committed Sep 08, 2010 155 156 157 158 159 160 161 162 163 \section{Drivers of external provers} \section{Transformations} \subsection{Non-splitting transformations} \begin{description} \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr}  MARCHE Claude committed Sep 09, 2010 164 165 166 \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 167 168 169 \item[eliminate\_definition] \item[eliminate\_definition\_func] \item[eliminate\_definition\_pred]  MARCHE Claude committed Sep 09, 2010 170 171 172 173 174 \item[eliminate\_if\_fmla] replaces formulas of the form if f1 then f2 else f3 by an equivalent formula using implications and other connectives. (TODO: detail) \item[eliminate\_if\_term] replaces terms of the form if formula then t2 else t3 by lift it at the level of the formula (TODO: detail)  MARCHE Claude committed Sep 08, 2010 175 \item[eliminate\_if]  MARCHE Claude committed Sep 09, 2010 176 177 178 179  apply both two above transformations \item[eliminate\_inductive] replaces inductive predicates by (incomplete) axiomatic definitions, i.e construction axioms and an inversion axiom (TODO: detail)  MARCHE Claude committed Sep 08, 2010 180 181 \item[eliminate\_let\_fmla] \item[eliminate\_let\_term]  MARCHE Claude committed Sep 09, 2010 182 183 \item[eliminate\_let] apply both two above transformations  MARCHE Claude committed Sep 08, 2010 184 185 186 187 188 189 \item[eliminate\_mutual\_recursion] \item[eliminate\_recursion] \item[encoding\_decorate\_mono] \item[encoding\_enumeration] \item[encoding\_simple2] \item[encoding\_smt]  MARCHE Claude committed Sep 08, 2010 190 Should we cite \cite{conchon08smt} here?  MARCHE Claude committed Sep 08, 2010 191 192 193 194 195 196 197 \item[encoding\_tptp] \item[filter\_trigger] \item[filter\_trigger\_builtin] \item[filter\_trigger\_no\_predicate] \item[hypothesis\_selection] \item[inline\_all] \item[inline\_trivial]  MARCHE Claude committed Sep 09, 2010 198 199 200 201  removes definitions of the form \begin{verbatim} logic f x_1 .. x_n = (g e_1 .. e_k) \end{verbatim}  MARCHE Claude committed Sep 10, 2010 202 203 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$  MARCHE Claude committed Sep 09, 2010 204   MARCHE Claude committed Sep 08, 2010 205 206 \item[remove\_triggers] \item[simplify\_array]  MARCHE Claude committed Sep 09, 2010 207 208 209 \item[simplify\_formula] reduces trivial equalities $t=t$ to True and then simplifies propositional structure: removes True, False, f and f'' to f'', etc.  MARCHE Claude committed Sep 08, 2010 210 \item[simplify\_recursive\_definition]  MARCHE Claude committed Sep 09, 2010 211 212 213 214 215 216 217 218 219 220 221 222 223  reduces mutually recursive definitions if they are not really mutually recursive, e.g.: \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 committed Sep 08, 2010 224 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240  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 committed Sep 08, 2010 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 \item[simplify\_trivial\_quantification\_in\_goal] \item[split\_premise] \end{description} \subsection{Splitting transformations} \begin{description} \item[right\_split] \item[simplify\_formula\_and\_task] \item[split\_all] \item[split\_goal] \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 committed Sep 06, 2010 260   MARCHE Claude committed Sep 06, 2010 261 262 263 264 265 266  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: