manpages.tex 4.77 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
\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
21
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
add    
MARCHE Claude committed
23
24
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
25
26
27
28
29
30
31
\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
add    
MARCHE Claude committed
32
\item TODO Claude: sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
33
34
\end{itemize}

MARCHE Claude's avatar
add    
MARCHE Claude committed
35
36
37
38
39
40
41
42
\subsection{Local use, without installation}

\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
commands are available in subdirectory \texttt{bin/}.

MARCHE Claude's avatar
MARCHE Claude committed
43
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
44

MARCHE Claude's avatar
add    
MARCHE Claude committed
45
46
47
48
49
50
51
52
53
54
why-config

ou 

IDE/Detect provers

Provers which are auto-detected: (share/prover-detection-data)

pour chaque prouveur:  lien sur page why/prover tips.

MARCHE Claude's avatar
doc    
MARCHE Claude committed
55
56
57
58
59
60
\section{The \texttt{why3} command-line tool}

\section{The \texttt{why3ml} tool}

\section{The \texttt{why3ide} tool}

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

MARCHE Claude's avatar
MARCHE Claude committed
63
64
65
66
67
68
69
70
71
\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}
72
73
74
\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
75
76
77
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
78
79
80
81
82
\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
83
\item[eliminate\_if]
84
85
86
87
  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
88
89
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
90
91
\item[eliminate\_let]
  apply both two above transformations
MARCHE Claude's avatar
MARCHE Claude committed
92
93
94
95
96
97
\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
98
Should we cite \cite{conchon08smt} here?
MARCHE Claude's avatar
MARCHE Claude committed
99
100
101
102
103
104
105
\item[encoding\_tptp]
\item[filter\_trigger]
\item[filter\_trigger\_builtin]
\item[filter\_trigger\_no\_predicate]
\item[hypothesis\_selection]
\item[inline\_all]
\item[inline\_trivial]
106
107
108
109
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
110
111
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$ 
112

MARCHE Claude's avatar
MARCHE Claude committed
113
114
\item[remove\_triggers]
\item[simplify\_array]
115
116
117
\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
118
\item[simplify\_recursive\_definition]
119
120
121
122
123
124
125
126
127
128
129
130
131
  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
132
\item[simplify\_trivial\_quantification]
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
  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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
\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
168

MARCHE Claude's avatar
doc    
MARCHE Claude committed
169
170
171
172
173
174

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