technical.tex 14.9 KB
Newer Older
1 2 3 4 5 6 7 8 9
\chapter{Technical Informations}


\section{Structure of Session Files}

The proof session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
10
\lstinputlisting{../share/why3session.dtd}
11 12


13
\section{Prover Detection}
14 15
\label{sec:proverdetecttiondata}

16
All the necessary data configuration for the automatic detection of
17 18 19 20
installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
file is reproduced below.
21 22 23 24 25 26 27
%BEGIN LATEX
{\footnotesize
%END LATEX
\lstinputlisting{../share/provers-detection-data.conf}
%BEGIN LATEX
}
%END LATEX
28

29
\section{The \texttt{why3.conf} Configuration File}
30 31 32
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
One can use a custom configuration file. The \why
tools look for it in the following order:
\begin{enumerate}
\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 the top directory of \why sources.
\end{enumerate}
If none of these files exist, a built-in default configuration is used.

The configuration file is a human-readable text file, which consists
of association pairs arranged in sections.
%BEGIN LATEX
Figure~\ref{fig:why3conf} shows an example of configuration file.
%END LATEX
%HEVEA Below is an example of configuration file.

52
%BEGIN LATEX
53
\begin{figure}[p]
54
{\footnotesize
55
%END LATEX
56
\begin{verbatim}
57
[main]
58
loadpath = "/usr/local/share/why3/theories"
59
loadpath = "/usr/local/share/why3/modules"
60
magic = 14
61
memlimit = 0
62 63 64 65 66
plugin = "/usr/local/lib/why3/plugins/tptp"
plugin = "/usr/local/lib/why3/plugins/genequlin"
plugin = "/usr/local/lib/why3/plugins/hypothesis_selection"
running_provers_max = 4
timelimit = 2
67

68
[ide]
69 70 71
default_editor = "editor %f"
error_color = "orange"
goal_color = "gold"
72
iconset = "boomy"
73 74 75 76 77 78 79 80
intro_premises = true
premise_color = "chartreuse"
print_labels = false
print_locs = false
print_time_limit = false
saving_policy = 2
task_height = 404
tree_width = 512
81
verbose = 0
82 83
window_height = 1173
window_width = 1024
84

85 86
[prover]
command = "'why3-cpulimit' 0 %m -s coqtop -batch -I %l/coq-tactic -R %l/coq Why3 -l %f"
87 88
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
89
in_place = false
90
interactive = true
91
name = "Coq"
92 93
shortcut = "coq"
version = "8.3pl4"
94

95 96
[prover]
command = "'why3-cpulimit' %t %m -s alt-ergo %f"
97
driver = "/usr/local/share/why3/drivers/alt_ergo_0.93.drv"
98
editor = ""
99
in_place = false
100
interactive = false
101
name = "Alt-Ergo"
102 103 104 105 106 107 108
shortcut = "altergo"
shortcut = "alt-ergo"
version = "0.93.1"

[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
name = "CoqIDE"
109
\end{verbatim}
110
%BEGIN LATEX
111
}
112
\caption{Sample \texttt{why3.conf} file}
113 114
\label{fig:why3conf}
\end{figure}
115
%END LATEX
116 117 118 119 120 121 122 123

A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
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.

124
Sections contain associations \texttt{key=value}. A value is either
125 126 127
an integer (\eg \texttt{-555}), a boolean (\texttt{true}, \texttt{false}),
or a string (\eg \texttt{"emacs"}). Some specific keys can be attributed
multiple values and are
128 129
thus allowed to occur several times inside a given section. In that
case, the relative order of these associations matter.
130

131
\section{Drivers for External Provers}
132 133
\label{sec:drivers}

134
Drivers for external provers are readable files from directory
135 136 137 138 139 140 141 142 143
\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]

\section{Transformations}
\label{sec:transformations}

144 145 146 147 148
This section documents the available transformations. We first
describe the most important ones, and then we provide a quick
documentation of the others, first the non-splitting ones, \eg those
which produce exactly one goal as result, and the others which produce any
number of goals.
149 150 151 152 153 154

Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
155
\index{list-transforms@\verb+--list-transforms+}
156

157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
\subsection{Inlining definitions}

Those transformations generally amount to replace some applications of
function or predicate symbols with its definition.

\begin{description}

\item[inline\_trivial]
  expands and removes definitions of the form
\begin{whycode}
function  f x_1 ... x_n = (g e_1 ... e_k)
predicate p x_1 ... x_n = (q e_1 ... e_k)
\end{whycode}
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1 \dots x_n$ occurs at most once in all the $e_i$.
172
\index{inline-trivial@\verb+inline_trivial+}
173 174 175

\item[inline\_goal] expands all outermost symbols of the goal that
  have a non-recursive definition.
176
\index{inline-goal@\verb+inline_goal+}
177 178 179

\item[inline\_all]
  expands all non-recursive definitions.
180
\index{inline-all@\verb+inline_all+}
181 182 183 184 185 186

\end{description}


\subsection{Induction Transformations}

187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
\begin{description}
\item[induction\_ty\_lex]:
  \index{induction-ty-lex@\verb+induction_ty_lex+}
  This transformation performs structural, lexicographic induction on
  goals involving universally quantified variables of algebraic data
  types, such as lists, trees, etc. For instance, it transforms the
  following goal
\begin{whycode}
goal G: forall l: list 'a. length l >= 0
\end{whycode}
  into this one:
\begin{whycode}
goal G :
  forall l:list 'a.
     match l with
     | Nil -> length l >= 0
     | Cons a l1 -> length l1 >= 0 -> length l >= 0
     end
\end{whycode}
  When induction can be applied to several variables, the transformation
MARCHE Claude's avatar
MARCHE Claude committed
207 208
  picks one heuristically. A label \verb|"induction"| can be used to
  force induction over one particular variable, \eg with
209 210 211 212
\begin{whycode}
goal G: forall l1 "induction" l2 l3: list 'a.
        l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215
induction will be applied on \verb|l1|. If this label is attached on
several variables, a lexicographic induction is performed on these
variables, from left to right.
216

MARCHE Claude's avatar
MARCHE Claude committed
217
%\item[] Induction on inductive predicates.
218

MARCHE Claude's avatar
MARCHE Claude committed
219 220 221
%[TO BE COMPLETED]

% TODO: implement also induction on int !
222

223
\end{description}
224 225 226

\subsection{Simplification by Computation}

227
These transformations simplify the goal by applying several kinds of
MARCHE Claude's avatar
MARCHE Claude committed
228 229 230 231 232 233
simplification, described below. The transformations differ only by
the kind of rules they apply:
\begin{description}
\item[compute\_in\_goal] aggressively applies all known
  computation/simplification rules
  \index{compute-in-goal@\verb+compute_in_goal+}
Martin Clochard's avatar
Martin Clochard committed
234

MARCHE Claude's avatar
MARCHE Claude committed
235 236 237 238
\item[compute\_specified] performs rewriting using only built-in
  operators and user-provided rules
  \index{compute-specified@\verb+compute_specified+}
\end{description}
Martin Clochard's avatar
Martin Clochard committed
239

MARCHE Claude's avatar
MARCHE Claude committed
240
The kinds of simplification are as follows.
241 242 243 244
\begin{itemize}
\item Computations with built-in symbols, \eg operations on integers,
  when applied to explicit constants, are evaluated. This includes
  evaluation of equality when a decision can be made (on integer
Martin Clochard's avatar
Martin Clochard committed
245 246 247 248 249
  constants, on constructors of algebraic data types), Boolean
  evaluation, simplification of pattern-matching/conditional expression,
  extraction of record fields, and beta-reduction.
  At best, these computations reduce the goal to
  \verb|true| and the transformations thus does not produce any sub-goal.
250
  For example, a goal
Martin Clochard's avatar
Martin Clochard committed
251 252 253 254 255
  like \verb|6*7=42| is solved by those transformations.
\item Unfolding of definitions, as done by \verb|inline_goal|.
  \verb|compute_in_goal| unfold all definitions, including recursive ones.
  For \verb|compute_specified|, the user can enable unfolding of a specific
  logic symbol by attaching the meta \verb|rewrite_def| to the symbol.
256 257 258 259 260
\begin{whycode}
function sqr (x:int) : int = x * x
meta "rewrite_def" function sqr
\end{whycode}
\item Rewriting using axioms or lemmas declared as rewrite rules. When
261
  an axiom (or a lemma) has one of the forms
262
\begin{whycode}
263
axiom a: forall ... t1 = t2
264 265 266
\end{whycode}
  or
\begin{whycode}
267
axiom a: forall ... f1 <-> f2
268 269 270
\end{whycode}
  then the user can declare
\begin{whycode}
271
meta "rewrite" axiom a
272
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
273
  to turn this axiom into a rewrite rule. Rewriting is always done
274 275
  from left to right. Beware that there is no check for termination
  nor for confluence of the set of rewrite rules declared.
MARCHE Claude's avatar
MARCHE Claude committed
276 277 278 279 280 281 282 283
\end{itemize}

\paragraph{Bound on the number of reductions}
The computations performed by these transformations can take an
arbitrarily large number of steps, or even not terminate. For this
reason, the number of steps is bounded by a maximal value, which is
set by default to 1000. This value can be increased by another meta,
\eg
284 285 286
\begin{whycode}
meta "compute_max_steps" 1_000_000
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
287 288
When this upper limit is reached, a warning is issued, and the
partly-reduced goal is returned as the result of the transformation.
289 290 291


\subsection{Other Non-Splitting Transformations}
292 293 294

\begin{description}

295 296
\item[eliminate\_algebraic] replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}.
297
\index{eliminate-algebraic@\verb+eliminate_algebraic+}
298

299
\item[eliminate\_builtin] removes definitions of symbols that are
300
  declared as builtin in the driver, \ie with a ``syntax'' rule.
301 302
\index{eliminate-builtin@\verb+eliminate_builtin+}

303
\item[eliminate\_definition\_func]
304
  replaces all function definitions with axioms.
305 306
\index{eliminate-definition-func@\verb+eliminate_definition_func+}

307
\item[eliminate\_definition\_pred]
308
  replaces all predicate definitions with axioms.
309 310
\index{eliminate-definition-pred@\verb+eliminate_definition_pred+}

311
\item[eliminate\_definition]
312
  applies both transformations above.
313 314
\index{eliminate-definition@\verb+eliminate_definition+}

315
\item[eliminate\_mutual\_recursion]
316
  replaces mutually recursive definitions with axioms.
317 318
\index{eliminate-mutual-recursion@\verb+eliminate_mutual_recursion+}

319
\item[eliminate\_recursion]
320
  replaces all recursive definitions with axioms.
321
\index{eliminate-recursion@\verb+eliminate_recursion+}
322 323 324 325

\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.
326
\index{eliminate-if-term@\verb+eliminate_if_term+}
327 328 329 330

\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
  else f3} by an equivalent formula using implications and other
  connectives.
331
\index{eliminate-if-fmla@\verb+eliminate_if_fmla+}
332 333

\item[eliminate\_if]
334
  applies both transformations above.
335
\index{eliminate-if@\verb+eliminate_if+}
336 337

\item[eliminate\_inductive] replaces inductive predicates by
338
  (incomplete) axiomatic definitions, \ie construction axioms and
339
  an inversion axiom.
340
\index{eliminate-inductive@\verb+eliminate_inductive+}
341 342

\item[eliminate\_let\_fmla]
343
  eliminates \texttt{let} by substitution, at the predicate level.
344
\index{eliminate-let-fmla@\verb+eliminate_let_fmla+}
345 346

\item[eliminate\_let\_term]
347
  eliminates \texttt{let} by substitution, at the term level.
348
\index{eliminate-let-term@\verb+eliminate_let_term+}
349 350

\item[eliminate\_let]
351
  applies both transformations above.
352
\index{eliminate-let@\verb+eliminate_let+}
353 354 355 356 357 358

% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]

\item[encoding\_smt]
359
  encodes polymorphic types into monomorphic type~\cite{conchon08smt}.
360
\index{encoding-smt@\verb+encoding_smt+}
361 362

\item[encoding\_tptp]
363
  encodes theories into unsorted logic. %~\cite{cruanes10}.
364
\index{encoding-tptp@\verb+encoding_tptp+}
365 366 367 368 369 370 371 372 373 374 375 376

% \item[filter\_trigger] *)

% \item[filter\_trigger\_builtin] *)

% \item[filter\_trigger\_no\_predicate] *)

% \item[hypothesis\_selection] *)
%   Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *)

\item[introduce\_premises] moves antecedents of implications and
  universal quantifications of the goal into the premises of the task.
377
\index{introduce-premises@\verb+introduce_premises+}
378 379 380 381

% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)

382
\item[simplify\_array] automatically rewrites the task using the lemma
383 384
  \verb|Select_eq| of theory \verb|map.Map|.
\index{simplify-array@\verb+simplify_array+}
385 386

\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
387 388
  then simplifies propositional structure: removes true, false, simplifies
  $f \land f$ to $f$, etc.
389
\index{simplify-formula@\verb+simplify_formula+}
390 391

\item[simplify\_recursive\_definition] reduces mutually recursive
392
  definitions if they are not really mutually recursive, \eg
393
\begin{whycode}
394
function f : ... = .... g ...
395 396
with g : ... = e
\end{whycode}
397
becomes
398 399 400 401 402
\begin{whycode}
function g : ... = e
function f : ... = ... g ...
\end{whycode}
if $f$ does not occur in $e$.
403
\index{simplify-recursive-definition@\verb+simplify_recursive_definition+}
404 405 406

\item[simplify\_trivial\_quantification]
  simplifies quantifications of the form
407
\begin{whycode}
408
forall x, x=t -> P(x)
409
\end{whycode}
410
or
411
\begin{whycode}
412
forall x, t=x -> P(x)
413
\end{whycode}
414
when $x$ does not occur in $t$ into
415
\begin{whycode}
416
P(t)
417
\end{whycode}
418
  More generally, it applies this simplification whenever $x=t$ appears
419
  in a negative position.
420
\index{simplify-trivial-quantification@\verb+simplify_trivial_quantification+}
421 422

\item[simplify\_trivial\_quantification\_in\_goal]
423
  is the same as above but it applies only in the goal.
424
\index{simplify-trivial-quantification-in-goal@\verb+simplify_trivial_quantification_in_goal+}
425 426 427

\item[split\_premise]
  splits conjunctive premises.
428
\index{split-premise@\verb+split_premise+}
429 430 431

\end{description}

432
\subsection{Other Splitting Transformations}
433 434 435 436

\begin{description}

\item[full\_split\_all]
437
  performs both \texttt{split\_premise} and \texttt{full\_split\_goal}.
438
\index{full-split-all@\verb+full_split_all+}
439 440 441 442

\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.
443
\index{full-split-goal@\verb+full_split_goal+}
444

445 446
\item[simplify\_formula\_and\_task] is the same as \texttt{simplify\_formula}
  but it also removes the goal if it is equivalent to true.
447
\index{full-split-all@\verb+full_split_all+}
448 449

\item[split\_all]
450
  performs both \texttt{split\_premise} and \texttt{split\_goal}.
451
\index{split-all@\verb+split_all+}
452 453 454 455

\item[split\_goal] if the goal is a conjunction of goals, returns the
  corresponding set of subgoals. The number of subgoals generated is linear in
  the size of the initial goal.
456
\index{split-goal@\verb+split_goal+}
457 458

\item[split\_intro]
459
  moves the antecedents into the premises when a goal is an implication.
460
\index{split-intro@\verb+split_intro+}
461 462 463 464 465 466 467 468 469 470

\end{description}


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