\chapter{Technical Informations}
\section{Structure of Session Files}
The proof 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.
\lstinputlisting{../share/why3session.dtd}
\section{Prover Detection}
\label{sec:proverdetecttiondata}
All the necessary data configuration for the automatic detection of
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.
%BEGIN LATEX
{\footnotesize
%END LATEX
\lstinputlisting{../share/provers-detection-data.conf}
%BEGIN LATEX
}
%END LATEX
\section{The \texttt{why3.conf} Configuration File}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
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.
%BEGIN LATEX
\begin{figure}[p]
{\footnotesize
%END LATEX
\begin{verbatim}
[main]
loadpath = "/usr/local/share/why3/theories"
loadpath = "/usr/local/share/why3/modules"
magic = 14
memlimit = 0
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
[ide]
default_editor = "editor %f"
error_color = "orange"
goal_color = "gold"
iconset = "boomy"
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
verbose = 0
window_height = 1173
window_width = 1024
[prover]
command = "'why3-cpulimit' 0 %m -s coqtop -batch -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
in_place = false
interactive = true
name = "Coq"
shortcut = "coq"
version = "8.3pl4"
[prover]
command = "'why3-cpulimit' %t %m -s alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo_0.93.drv"
editor = ""
in_place = false
interactive = false
name = "Alt-Ergo"
shortcut = "altergo"
shortcut = "alt-ergo"
version = "0.93.1"
[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
name = "CoqIDE"
\end{verbatim}
%BEGIN LATEX
}
\caption{Sample \texttt{why3.conf} file}
\label{fig:why3conf}
\end{figure}
%END LATEX
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.
Sections contain associations \texttt{key=value}. A value is either
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
thus allowed to occur several times inside a given section. In that
case, the relative order of these associations matter.
\section{Drivers for External Provers}
\label{sec:drivers}
Drivers for external provers are readable files from 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]
\section{Transformations}
\label{sec:transformations}
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.
Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
\index{list-transforms@\verb+--list-transforms+}
\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$.
\index{inline-trivial@\verb+inline_trivial+}
\item[inline\_goal] expands all outermost symbols of the goal that
have a non-recursive definition.
\index{inline-goal@\verb+inline_goal+}
\item[inline\_all]
expands all non-recursive definitions.
\index{inline-all@\verb+inline_all+}
\end{description}
\subsection{Induction Transformations}
\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
picks one heuristically. A label \verb|"induction"| can be used to
force induction over one particular variable, \eg with
\begin{whycode}
goal G: forall l1 "induction" l2 l3: list 'a.
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode}
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.
%\item[] Induction on inductive predicates.
%[TO BE COMPLETED]
% TODO: implement also induction on int !
\end{description}
\subsection{Simplification by Computation}
These transformations simplify the goal by applying several kinds of
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+}
\item[compute\_specified] performs rewriting using only built-in
operators and user-provided rules
\index{compute-specified@\verb+compute_specified+}
\end{description}
The kinds of simplification are as follows.
\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
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.
For example, a goal
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.
\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
an axiom (or a lemma) has one of the forms
\begin{whycode}
axiom a: forall ... t1 = t2
\end{whycode}
or
\begin{whycode}
axiom a: forall ... f1 <-> f2
\end{whycode}
then the user can declare
\begin{whycode}
meta "rewrite" axiom a
\end{whycode}
to turn this axiom into a rewrite rule. Rewriting is always done
from left to right. Beware that there is no check for termination
nor for confluence of the set of rewrite rules declared.
\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
\begin{whycode}
meta "compute_max_steps" 1_000_000
\end{whycode}
When this upper limit is reached, a warning is issued, and the
partly-reduced goal is returned as the result of the transformation.
\subsection{Other Non-Splitting Transformations}
\begin{description}
\item[eliminate\_algebraic] replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}.
\index{eliminate-algebraic@\verb+eliminate_algebraic+}
\item[eliminate\_builtin] removes definitions of symbols that are
declared as builtin in the driver, \ie with a ``syntax'' rule.
\index{eliminate-builtin@\verb+eliminate_builtin+}
\item[eliminate\_definition\_func]
replaces all function definitions with axioms.
\index{eliminate-definition-func@\verb+eliminate_definition_func+}
\item[eliminate\_definition\_pred]
replaces all predicate definitions with axioms.
\index{eliminate-definition-pred@\verb+eliminate_definition_pred+}
\item[eliminate\_definition]
applies both transformations above.
\index{eliminate-definition@\verb+eliminate_definition+}
\item[eliminate\_mutual\_recursion]
replaces mutually recursive definitions with axioms.
\index{eliminate-mutual-recursion@\verb+eliminate_mutual_recursion+}
\item[eliminate\_recursion]
replaces all recursive definitions with axioms.
\index{eliminate-recursion@\verb+eliminate_recursion+}
\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.
\index{eliminate-if-term@\verb+eliminate_if_term+}
\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.
\index{eliminate-if-fmla@\verb+eliminate_if_fmla+}
\item[eliminate\_if]
applies both transformations above.
\index{eliminate-if@\verb+eliminate_if+}
\item[eliminate\_inductive] replaces inductive predicates by
(incomplete) axiomatic definitions, \ie construction axioms and
an inversion axiom.
\index{eliminate-inductive@\verb+eliminate_inductive+}
\item[eliminate\_let\_fmla]
eliminates \texttt{let} by substitution, at the predicate level.
\index{eliminate-let-fmla@\verb+eliminate_let_fmla+}
\item[eliminate\_let\_term]
eliminates \texttt{let} by substitution, at the term level.
\index{eliminate-let-term@\verb+eliminate_let_term+}
\item[eliminate\_let]
applies both transformations above.
\index{eliminate-let@\verb+eliminate_let+}
% \item[encoding\_decorate\_mono]
% \item[encoding\_enumeration]
\item[encoding\_smt]
encodes polymorphic types into monomorphic type~\cite{conchon08smt}.
\index{encoding-smt@\verb+encoding_smt+}
\item[encoding\_tptp]
encodes theories into unsorted logic. %~\cite{cruanes10}.
\index{encoding-tptp@\verb+encoding_tptp+}
% \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.
\index{introduce-premises@\verb+introduce_premises+}
% \item[remove\_triggers] *)
% removes the triggers in all quantifications. *)
\item[simplify\_array] automatically rewrites the task using the lemma
\verb|Select_eq| of theory \verb|map.Map|.
\index{simplify-array@\verb+simplify_array+}
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
then simplifies propositional structure: removes true, false, simplifies
$f \land f$ to $f$, etc.
\index{simplify-formula@\verb+simplify_formula+}
\item[simplify\_recursive\_definition] reduces mutually recursive
definitions if they are not really mutually recursive, \eg
\begin{whycode}
function f : ... = .... g ...
with g : ... = e
\end{whycode}
becomes
\begin{whycode}
function g : ... = e
function f : ... = ... g ...
\end{whycode}
if $f$ does not occur in $e$.
\index{simplify-recursive-definition@\verb+simplify_recursive_definition+}
\item[simplify\_trivial\_quantification]
simplifies quantifications of the form
\begin{whycode}
forall x, x=t -> P(x)
\end{whycode}
or
\begin{whycode}
forall x, t=x -> P(x)
\end{whycode}
when $x$ does not occur in $t$ into
\begin{whycode}
P(t)
\end{whycode}
More generally, it applies this simplification whenever $x=t$ appears
in a negative position.
\index{simplify-trivial-quantification@\verb+simplify_trivial_quantification+}
\item[simplify\_trivial\_quantification\_in\_goal]
is the same as above but it applies only in the goal.
\index{simplify-trivial-quantification-in-goal@\verb+simplify_trivial_quantification_in_goal+}
\item[split\_premise]
splits conjunctive premises.
\index{split-premise@\verb+split_premise+}
\end{description}
\subsection{Other Splitting Transformations}
\begin{description}
\item[full\_split\_all]
performs both \texttt{split\_premise} and \texttt{full\_split\_goal}.
\index{full-split-all@\verb+full_split_all+}
\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.
\index{full-split-goal@\verb+full_split_goal+}
\item[simplify\_formula\_and\_task] is the same as \texttt{simplify\_formula}
but it also removes the goal if it is equivalent to true.
\index{full-split-all@\verb+full_split_all+}
\item[split\_all]
performs both \texttt{split\_premise} and \texttt{split\_goal}.
\index{split-all@\verb+split_all+}
\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.
\index{split-goal@\verb+split_goal+}
\item[split\_intro]
moves the antecedents into the premises when a goal is an implication.
\index{split-intro@\verb+split_intro+}
\end{description}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: