\chapter{Technical Informations}
%HEVEA\cutname{technical.html}
\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}
The 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 content of this
file is reproduced below.
%BEGIN LATEX
{\footnotesize
%END LATEX
\lstinputlisting[language={},morecomment={[l]\#},morestring={[b]"}]{../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.
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 a single
identifier, \eg \texttt{[main]}, or it can be composed by a family name
and a single family argument, \eg \texttt{[prover alt-ergo]}.
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 matters.
\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+}
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. The \verb|[@induction]| attribute 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 attribute is attached to
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|. Transformation
\verb|compute_in_goal| unfolds 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" prop 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}
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the \verb|[@rewrite]| attribute on the axiom name or
on the axiom itself, e.g.:
\begin{whycode}
axiom a [@rewrite]: forall ... t1 = t2
lemma b: [@rewrite] forall ... f1 <-> f2
\end{whycode}
The second form allows some form of local rewriting, e.g.
\begin{whycode}
lemma l: forall x y. ([@rewrite] x = y) -> f x = f y
\end{whycode}
can be proved by \verb|introduce_premises| followed by \verb|compute_specified|.
\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 types~\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}
into
\begin{whycode}
P(t)
\end{whycode}
when $x$ does not occur in $t$.
More generally, this simplification is applied whenever $x=t$ or
$t=x$ appears in 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] replaces axioms in conjunctive form
by an equivalent collection of axioms.
In absence of case analysis attributes (see \texttt{split\_goal} for details),
the number of axiom generated per initial axiom is
linear in the size of that initial axiom.
\index{split-premise@\verb+split_premise+}
\item[split\_premise\_full] is similar to \texttt{split\_premise}, but it
also converts the axioms to conjunctive normal form. The number of
axioms generated per initial axiom may be exponential in the size of
the initial axiom.
\index{split-premise-full@\verb+split_premise_full+}
\end{description}
\subsection{Other Splitting Transformations}
\label{tech:trans:split}
\begin{description}
\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{simplify-formula-and-task@\verb+simplify_formula_and_task+}
\item[split\_goal] changes conjunctive goals into the
corresponding set of subgoals. In absence of case analysis attributes,
the number of subgoals generated is linear in the size of the initial goal.
\paragraph{Behavior on asymmetric connectives and
\texttt{by}/\texttt{so}}
The transformation treats specially asymmetric and
\texttt{by}/\texttt{so} connectives. Asymmetric conjunction
\verb|A && B| in goal position is handled as syntactic sugar for
\verb|A /\ (A -> B)|. The conclusion of the first subgoal can then
be used to prove the second one.
Asymmetric disjunction \verb+A || B+ in hypothesis position is handled as
syntactic sugar for \verb|A \/ ((not A) /\ B)|.
In particular, a case analysis on such hypothesis would give the negation of
the first hypothesis in the second case.
The \texttt{by} connective is treated as a proof indication. In
hypothesis position, \verb|A by B| is treated as if it were
syntactic sugar for its regular interpretation \verb|A|. In goal
position, it is treated as if \verb|B| was an intermediate step for
proving \verb|A|. \verb|A by B| is then replaced by \verb|B| and the
transformation also generates a side-condition subgoal \verb|B -> A|
representing the logical cut.
Although splitting stops at disjunctive points like symmetric
disjunction and left-hand sides of implications, the occurrences of
the \texttt{by} connective are not restricted. For instance:
\begin{itemize}
\item Splitting
\begin{whycode}
goal G : (A by B) && C
\end{whycode}
generates the subgoals
\begin{whycode}
goal G1 : B
goal G2 : A -> C
goal G3 : B -> A (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : (A by B) \/ (C by D)
\end{whycode}
generates
\begin{whycode}
goal G1 : B \/ D
goal G2 : B -> A (* side-condition *)
goal G3 : D -> C (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : (A by B) || (C by D)
\end{whycode}
generates
\begin{whycode}
goal G1 : B || D
goal G2 : B -> A (* side-condition *)
goal G3 : B || (D -> C) (* side-condition *)
\end{whycode}
Note that due to the asymmetric disjunction, the disjunction is kept in the
second side-condition subgoal.
\item Splitting
\begin{whycode}
goal G : exists x. P x by x = 42
\end{whycode}
generates
\begin{whycode}
goal G1 : exists x. x = 42
goal G2 : forall x. x = 42 -> P x (* side-condition *)
\end{whycode}
Note that in the side-condition subgoal, the context is universally closed.
\end{itemize}
The \texttt{so} connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, \verb|A so B| is treated as if it were syntactic sugar for its regular interpretation \verb|A|. In hypothesis position, it is treated as if both \verb|A| and \verb|B| were true because \verb|B| is a consequence of \verb|A|. \verb|A so B| is replaced by \verb|A /\ B| and the transformation also generates a side-condition subgoal \verb|A -> B| corresponding to the consequence relation between formula.
As with the \texttt{by} connective, occurrences of \texttt{so} are
unrestricted. For instance:
\begin{itemize}
\item Splitting
\begin{whycode}
goal G : (((A so B) \/ C) -> D) && E
\end{whycode}
generates
\begin{whycode}
goal G1 : ((A /\ B) \/ C) -> D
goal G2 : (A \/ C -> D) -> E
goal G3 : A -> B (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : A by exists x. P x so Q x so R x by T x
(* reads: A by (exists x. P x so (Q x so (R x by T x))) *)
\end{whycode}
generates
\begin{whycode}
goal G1 : exists x. P x
goal G2 : forall x. P x -> Q x (* side-condition *)
goal G3 : forall x. P x -> Q x -> T x (* side-condition *)
goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *)
goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *)
\end{whycode}
In natural language, this corresponds to the following proof scheme
for \verb|A|: There exists a \verb|x| for which \verb|P| holds. Then,
for that witness \verb|Q| and \verb|R| also holds. The last one holds
because \verb|T| holds as well. And from those three conditions on
\verb|x|, we can deduce \verb|A|.
\end{itemize}
\paragraph{Attributes controlling the transformation}
The transformations in the split family can be controlled by using
attributes on formulas.
The \verb|[@stop_split]| attribute can be used to block the splitting of a
formula. The attribute is removed after blocking, so applying the
transformation a second time will split the formula. This is can be
used to decompose the splitting process in several steps. Also, if a
formula with this attribute is found in non-goal position, its
\texttt{by}/\texttt{so} proof indication will be erased by the
transformation. In a sense, formulas tagged by \verb|[@stop_split]| are
handled as if they were local lemmas.
The \verb|[@case_split]| attribute can be used to force case analysis on hypotheses.
For instance, applying \texttt{split\_goal} on
\begin{whycode}
goal G : ([@case_split] A \/ B) -> C
\end{whycode}
generates the subgoals
\begin{whycode}
goal G1 : A -> C
goal G2 : B -> C
\end{whycode}
Without the attribute, the transformation does nothing because undesired case analysis
may easily lead to an exponential blow-up.
Note that the precise behavior of splitting transformations in presence of
the \verb|[@case_split]| attribute is not yet specified
and is likely to change in future versions.
\index{split-goal@\verb+split_goal+}
\item[split\_all]
performs both \texttt{split\_premise} and \texttt{split\_goal}.
\index{split-all@\verb+split_all+}
\item[split\_intro]
performs both \texttt{split\_goal} and \texttt{introduce\_premises}.
\index{split-intro@\verb+split_intro+}
\item[split\_goal\_full]
has a behavior similar
to \texttt{split\_goal}, but also converts the goal to conjunctive normal form.
The number of subgoals generated may be exponential in the size of the initial goal.
\index{split-goal-full@\verb+split_goal_full+}
\item[split\_all\_full]
performs both \texttt{split\_premise} and \texttt{split\_goal\_full}.
\index{split-all-full@\verb+split_all_full+}
\end{description}
\section{Proof Strategies}
\label{sec:strategies}
As seen in Section~\ref{sec:ideref}, the IDE provides a few buttons
that trigger the run of simple proof strategies on the selected goals.
Proof strategies can be defined using a basic assembly-style language,
and put into the Why3 configuration file. The commands of this basic
language are:
\begin{itemize}
\item \texttt{c $p$ $t$ $m$} calls the prover $p$ with a time limit
$t$ and memory limit $m$. On success, the strategy ends, it
continues to next line otherwise
\item \texttt{t $n$ $lab$} applies the transformation $n$. On success,
the strategy continues to label $lab$, and is applied to each
generated sub-goals. It continues to next line otherwise.
\item \texttt{g $lab$} inconditionally jumps to label $lab$
\item \texttt{$lab$:} declares the label $lab$. The default label
\texttt{exit} allows to stop the program.
\end{itemize}
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the \verb|why3 config --detect| command
\begin{description}
\item[Split] is bound to the 1-line strategy
\begin{verbatim}
t split_goal_wp exit
\end{verbatim}
\item[Auto level 0] is bound to
\begin{verbatim}
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
\end{verbatim}
The three provers are tried for a time limit of 1 second and memory
limit of 1~Gb, each in turn. This is a perfect strategy for a first
attempt to discharge a new goal.
\item[Auto level 1] is bound to
\begin{verbatim}
start:
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.5.0, 10 4000
c Alt-Ergo,1.30, 10 4000
c CVC4,1.5, 10 4000
\end{verbatim}
The three provers are first tried for a time limit of 1 second and
memory limit of 1~Gb, each in turn. If none of them succeed, a
split is attempted. If the split works then the same strategy is
retried on each sub-goals. If the split does not succeed, the provers
are tried again with a larger limits.
\item[Auto level 2] is bound to
\begin{verbatim}
start:
c Z3,4.5.0, 1 1000
c Eprover,2.0, 1 1000
c Spass,3.7, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.5.0, 5 2000
c Eprover,2.0, 5 2000
c Spass,3.7, 5 2000
c Alt-Ergo,1.30, 5 2000
c CVC4,1.5, 5 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_goal_wp start
trylongertime:
c Z3,4.5.0, 30 4000
c Eprover,2.0, 30 4000
c Spass,3.7, 30 4000
c Alt-Ergo,1.30, 30 4000
c CVC4,1.5, 30 4000
\end{verbatim}
Notice that now 5 provers are used. The provers are first tried for
a time limit of 1 second and memory limit of 1~Gb, each in turn. If
none of them succeed, a split is attempted. If the split works then
the same strategy is retried on each sub-goals. If the split does
not succeed, the prover are tried again with limits of 5 s and 2
Gb. If all fail, we attempt the transformation of introduction of
premises in the context, followed by an inlining of the definitions
in the goals. We then attempt a split again, if the split succeeds,
we restart from the beginning, if it fails then provers are tried
again with 30s and 4 Gb.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: