manpages.tex 4.37 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
5

\section{Compilation, Installation}

MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
32
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
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's avatar
MARCHE Claude committed
40
41
\section{The \texttt{why.conf} configuration file}

MARCHE Claude's avatar
MARCHE Claude committed
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}
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's avatar
MARCHE Claude committed
54
55
56
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
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's avatar
MARCHE Claude committed
62
\item[eliminate\_if]
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's avatar
MARCHE Claude committed
67
68
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
69
70
\item[eliminate\_let]
  apply both two above transformations
MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
biblio    
MARCHE Claude committed
77
Should we cite \cite{conchon08smt} here?
MARCHE Claude's avatar
MARCHE Claude committed
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]
85
86
87
88
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
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$ 
91

MARCHE Claude's avatar
MARCHE Claude committed
92
93
\item[remove\_triggers]
\item[simplify\_array]
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's avatar
MARCHE Claude committed
97
\item[simplify\_recursive\_definition]
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's avatar
MARCHE Claude committed
111
\item[simplify\_trivial\_quantification]
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
147

MARCHE Claude's avatar
doc    
MARCHE Claude committed
148
149
150
151
152
153

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