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
Newer Older
MARCHE Claude's avatar
doc    
MARCHE Claude committed
1
\chapter{Reference manuals for the Why3 tools}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:manpages}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
3
4

\section{Compilation, Installation}
MARCHE Claude's avatar
MARCHE Claude committed
5
\label{sec:install}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
8
9
10
11
12
13
Compilation of Why3 must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes you current configuration and check if requirements hold.
Compilation requires:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
14
15
16
\item The Objective Caml compiler, version 3.10 or higher. It is
  available as a binary package for most Unix distributions. For
  debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
17
18
19
20
21
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
It is also installable from sources, downloadable from the Web site
\url{http://caml.inria.fr/ocaml/}
MARCHE Claude's avatar
add    
MARCHE Claude committed
22
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
add    
MARCHE Claude committed
24
25
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
26
27
28
29
30
31
32
\item The Lablgtk2 library for Ocaml bindings of the gtk2 graphical library.
 For debian-based Linux distributions, you can install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site \url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}

MARCHE Claude's avatar
MARCHE Claude committed
33
34
35
36
37
38
39
\item The Ocaml bindings of the sqlite3 library
For debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
MARCHE Claude's avatar
MARCHE Claude committed
40
41
\end{itemize}

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

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

MARCHE Claude's avatar
MARCHE Claude committed
51
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
52

MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
add    
MARCHE Claude committed
57

MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
add    
MARCHE Claude committed
60

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

MARCHE Claude's avatar
MARCHE Claude committed
64
65
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
66

MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
add    
MARCHE Claude committed
105

MARCHE Claude's avatar
doc    
MARCHE Claude committed
106
107
108
109
110
\section{The \texttt{why3} command-line tool}

\section{The \texttt{why3ml} tool}

\section{The \texttt{why3ide} tool}
MARCHE Claude's avatar
MARCHE Claude committed
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[Edit] Start an editor on the selected task.

  For automatic provers, this allows to see the file sent to the
  prover.

  For interactive provers, this also allows to add or modify the
  corresponding proof script. The modifications are saved, and can be
  retrieved later even if the goal was modified.

\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's avatar
MARCHE Claude committed
146

MARCHE Claude's avatar
MARCHE Claude committed
147
148
149
150
\subsection{Preferences}

\subsection{Structure of the database file}

MARCHE Claude's avatar
MARCHE Claude committed
151
[TODO]
MARCHE Claude's avatar
doc    
MARCHE Claude committed
152

MARCHE Claude's avatar
MARCHE Claude committed
153
154
\section{The \texttt{why.conf} configuration file}

MARCHE Claude's avatar
MARCHE Claude committed
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}
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's avatar
MARCHE Claude committed
167
168
169
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
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's avatar
MARCHE Claude committed
175
\item[eliminate\_if]
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's avatar
MARCHE Claude committed
180
181
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
182
183
\item[eliminate\_let]
  apply both two above transformations
MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
biblio    
MARCHE Claude committed
190
Should we cite \cite{conchon08smt} here?
MARCHE Claude's avatar
MARCHE Claude committed
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]
198
199
200
201
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
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$ 
204

MARCHE Claude's avatar
MARCHE Claude committed
205
206
\item[remove\_triggers]
\item[simplify\_array]
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's avatar
MARCHE Claude committed
210
\item[simplify\_recursive\_definition]
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's avatar
MARCHE Claude committed
224
\item[simplify\_trivial\_quantification]
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
260

MARCHE Claude's avatar
doc    
MARCHE Claude committed
261
262
263
264
265
266

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