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 4.37 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 5  \section{Compilation, Installation}  MARCHE Claude committed Sep 07, 2010 6 7 8 9 10 11 12 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 13 14 15 \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 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 \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/} \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} \item TODO: sqlite3 \end{itemize}  MARCHE Claude committed Sep 06, 2010 32 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 33 34 35 36 37 38 39  \section{The \texttt{why3} command-line tool} \section{The \texttt{why3ml} tool} \section{The \texttt{why3ide} tool}  MARCHE Claude committed Sep 06, 2010 40 41 \section{The \texttt{why.conf} configuration file}  MARCHE Claude committed Sep 08, 2010 42 43 44 45 46 47 48 49 50 \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 51 52 53 \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 54 55 56 \item[eliminate\_definition] \item[eliminate\_definition\_func] \item[eliminate\_definition\_pred]  MARCHE Claude committed Sep 09, 2010 57 58 59 60 61 \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 62 \item[eliminate\_if]  MARCHE Claude committed Sep 09, 2010 63 64 65 66  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 67 68 \item[eliminate\_let\_fmla] \item[eliminate\_let\_term]  MARCHE Claude committed Sep 09, 2010 69 70 \item[eliminate\_let] apply both two above transformations  MARCHE Claude committed Sep 08, 2010 71 72 73 74 75 76 \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 77 Should we cite \cite{conchon08smt} here?  MARCHE Claude committed Sep 08, 2010 78 79 80 81 82 83 84 \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 85 86 87 88  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 89 90 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 91   MARCHE Claude committed Sep 08, 2010 92 93 \item[remove\_triggers] \item[simplify\_array]  MARCHE Claude committed Sep 09, 2010 94 95 96 \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 97 \item[simplify\_recursive\_definition]  MARCHE Claude committed Sep 09, 2010 98 99 100 101 102 103 104 105 106 107 108 109 110  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 111 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127  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 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 \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 147   MARCHE Claude committed Sep 06, 2010 148 149 150 151 152 153  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: