api.tex 15.1 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
\chapter{The \why API}
2
\label{chap:api}\index{API}
3
%HEVEA\cutname{api.html}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
4

5
This chapter is a tutorial for the users who want to link their own
MARCHE Claude's avatar
MARCHE Claude committed
6
OCaml code with the \why library. We progressively introduce the way
MARCHE Claude's avatar
MARCHE Claude committed
7 8
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
9 10 11
tasks. The complete documentation for API calls is given\begin{latexonly}
at URL~\urlapi{}.\end{latexonly}
%HEVEA at this \ahref{\urlapi}{URL}.
12

MARCHE Claude's avatar
MARCHE Claude committed
13
We assume the reader has a fair knowledge of the OCaml
MARCHE Claude's avatar
MARCHE Claude committed
14
language. Notice that the \why library must be installed, see
15
Section~\ref{sec:installlib}. The OCaml code given below is available in
MARCHE Claude's avatar
MARCHE Claude committed
16 17
the source distribution in directory \verb|examples/use_api/| together
with a few other examples.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
18

19
\lstset{language={[Objective]Caml}}
MARCHE Claude's avatar
MARCHE Claude committed
20 21 22 23 24

\section{Building Propositional Formulas}

The first step is to know how to build propositional formulas. The
module \texttt{Term} gives a few functions for building these. Here is
MARCHE Claude's avatar
MARCHE Claude committed
25 26
a piece of OCaml code for building the formula $\mathit{true} \lor
\mathit{false}$.
27
\lstinputlisting{generated/logic__opening.ml}
Andrei Paskevich's avatar
Andrei Paskevich committed
28
The library uses the common type \texttt{term} both for terms
29 30
(\ie expressions that produce a value of some particular type)
and formulas (\ie boolean-valued expressions).
Andrei Paskevich's avatar
Andrei Paskevich committed
31 32 33 34
% To distinguish terms from formulas, one can look at the
% \texttt{t_ty} field of the \texttt{term} record: in formulas,
% this field has the value \texttt{None}, and in terms,
% \texttt{Some t}, where \texttt{t} is of type \texttt{Ty.ty}.
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37

Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers.
38
\lstinputlisting{generated/logic__printformula.ml}
MARCHE Claude's avatar
MARCHE Claude committed
39 40 41 42

Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using
\begin{verbatim}
43
ocamlfind ocamlc -package why3 -linkpkg f.ml -o f
MARCHE Claude's avatar
MARCHE Claude committed
44 45 46
\end{verbatim}
Running the generated executable \texttt{f} results in the following output.
\begin{verbatim}
47
formula 1 is: true \/ false
MARCHE Claude's avatar
MARCHE Claude committed
48 49
\end{verbatim}

50
Let us now build a formula with propositional variables: $A \land B
MARCHE Claude's avatar
MARCHE Claude committed
51 52
\rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows.
53
\lstinputlisting{generated/logic__declarepropvars.ml}
Andrei Paskevich's avatar
Andrei Paskevich committed
54 55 56 57
The type \texttt{lsymbol} is the type of function and predicate symbols (which
we call logic symbols for brevity). Then the atoms $A$ and $B$ must be built
by the general function for applying a predicate symbol to a list of terms.
Here we just need the empty list of arguments.
58
\lstinputlisting{generated/logic__declarepropatoms.ml}
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61

As expected, the output is as follows.
\begin{verbatim}
62
formula 2 is: A /\ B -> A
MARCHE Claude's avatar
MARCHE Claude committed
63
\end{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
64 65 66 67
Notice that the concrete syntax of \why forbids function and predicate
names to start with a capital letter (except for the algebraic type
constructors which must start with one). This constraint is not enforced
when building those directly using library calls.
68

MARCHE Claude's avatar
MARCHE Claude committed
69
\section{Building Tasks}
70

71
Let us see how we can call a prover to prove a formula. As said in
72 73 74
previous chapters, a prover must be given a task, so we need to build
tasks from our formulas. Task can be build incrementally from an empty
task by adding declaration to it, using the functions
75 76
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor
\mathit{false}$ above, this is done as follows.
77
\lstinputlisting{generated/logic__buildtask.ml}
78
To make the formula a goal, we must give a name to it, here ``goal1''. A
79 80
goal name has type \texttt{prsymbol}, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete
MARCHE Claude's avatar
MARCHE Claude committed
81
syntax of \why requires these symbols to be capitalized, but it is not
82 83
mandatory when using the library. The second argument of
\texttt{add\_prop\_decl} is the kind of the proposition:
84 85 86
\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}.
Notice that lemmas are not allowed in tasks
and can only be used in theories.
87

88
Once a task is built, it can be printed.
89
\lstinputlisting{generated/logic__printtask.ml}
90

91
The task for our second formula is a bit more complex to build, because
92
the variables A and B must be added as abstract (\ie not defined)
Andrei Paskevich's avatar
Andrei Paskevich committed
93
propositional symbols in the task.
94
\lstinputlisting{generated/logic__buildtask2.ml}
95 96 97 98 99

Execution of our OCaml program now outputs:
\begin{verbatim}
task 1 is:
theory Task
100
  goal Goal1 : true \/ false
101 102 103 104
end

task 2 is:
theory Task
105
  predicate A
106

107
  predicate B
108

109
  goal Goal2 : A /\ B -> A
110 111 112 113
end
\end{verbatim}

\section{Calling External Provers}
114
\label{sec:api:callingprovers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
115

116
To call an external prover, we need to access the \why configuration
117
file \texttt{why3.conf}, as it was built using the \texttt{why3config}
118 119 120
command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this
configuration file.
121
\lstinputlisting{generated/logic__getconf.ml}
122
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
123 124 125
prover is a record with a name, a version, and an alternative description
(to differentiate between various configurations of a given prover). Its
definition is in the module \texttt{Whyconf}:
126
\lstinputlisting{generated/whyconf__provertype.ml}
127 128
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
129
attempt to access a prover named ``Alt-Ergo'', any version.
130
\lstinputlisting{generated/logic__getanyaltergo.ml}
131
We could also get a specific version with :
132
\lstinputlisting{generated/logic__getaltergo200.ml}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
133

MARCHE Claude's avatar
MARCHE Claude committed
134 135 136
The next step is to obtain the driver associated to this prover. A
driver typically depends on the standard theories so these should be
loaded first.
137
\lstinputlisting{generated/logic__getdriver.ml}
138 139 140

We are now ready to call the prover on the tasks. This is done by a
function call that launches the external executable and waits for its
141
termination. Here is a simple way to proceed:
142
\lstinputlisting{generated/logic__callprover.ml}
143
This way to call a prover is in general too naive, since it may never
MARCHE Claude's avatar
MARCHE Claude committed
144
return if the prover runs without time limit. The function
145 146
\texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined
in module \texttt{Call\_provers}:
147
\lstinputlisting{generated/call_provers__resourcelimit.ml}
148 149 150
where the field \texttt{limit\_time} is the maximum allowed running time in seconds,
and \texttt{limit\_mem} is the maximum allowed memory in megabytes.  The type
\texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:
151
\lstinputlisting{generated/call_provers__proverresult.ml}
152
with in particular the fields:
153
\begin{itemize}
154 155
\item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
156
\end{itemize}
157
A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:
158
\lstinputlisting{generated/call_provers__proveranswer.ml}
159
corresponding to these kinds of answers:
160 161 162
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover.
\item \texttt{Invalid}: the task is invalid.
163 164
\item \texttt{Timeout}: the prover exceeds the time limit.
\item \texttt{OutOfMemory}: the prover exceeds the memory limit.
MARCHE Claude's avatar
MARCHE Claude committed
165
\item \texttt{Unknown} $msg$: the prover can't determine if the task
166
  is valid; the string parameter $msg$ indicates some extra
MARCHE Claude's avatar
MARCHE Claude committed
167
  information.
168
\item \texttt{Failure} $msg$: the prover reports a failure, \eg it
MARCHE Claude's avatar
MARCHE Claude committed
169 170
  was unable to read correctly its input task.
\item \texttt{HighFailure}: an error occurred while trying to call the
171
  prover, or the prover answer was not understood (\eg none of the
172 173
  given regular expressions in the driver file matches the output
  of the prover).
174
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
175 176
Here is thus another way of calling the Alt-Ergo prover, on our second
task.
177
\lstinputlisting{generated/logic__calltimelimit.ml}
178 179 180 181 182 183 184
The output of our program is now as follows.
\begin{verbatim}
On task 1, alt-ergo answers Valid (0.01s)
On task 2, alt-ergo answers Valid in  0.01 seconds
\end{verbatim}

\section{Building Terms}
MARCHE Claude's avatar
MARCHE Claude committed
185 186 187 188 189

An important feature of the functions for building terms and formulas
is that they statically guarantee that only well-typed terms can be
constructed.

190
Here is the way we build the formula $2+2=4$. The main difficulty is to
191
access the internal identifier for addition: it must be retrieved from
Guillaume Melquiond's avatar
Guillaume Melquiond committed
192 193
the standard theory \texttt{Int} of the file \texttt{int.why}.
% (see Chap~\ref{sec:library}).
194
\lstinputlisting{generated/logic__buildfmla.ml}
195 196 197
An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed
the constructor \texttt{t\_app\_infer} infers the type of the resulting
198
term. One could also provide the expected type as follows.
199
\lstinputlisting{generated/logic__buildtermalt.ml}
200

201 202
When building a task with this formula, we need to declare that we use
theory \texttt{Int}:
203
\lstinputlisting{generated/logic__buildtaskimport.ml}
204 205 206

\section{Building Quantified Formulas}

207 208 209
To illustrate how to build quantified formulas, let us consider
the formula $\forall x:int. x*x \geq 0$. The first step is to
obtain the symbols from \texttt{Int}.
210
\lstinputlisting{generated/logic__quantfmla1.ml}
211
The next step is to introduce the variable $x$ with the type int.
212
\lstinputlisting{generated/logic__quantfmla2.ml}
213
The formula $x*x \geq 0$ is obtained as in the previous example.
214
\lstinputlisting{generated/logic__quantfmla3.ml}
215
To quantify on $x$, we use the appropriate smart constructor as follows.
216
\lstinputlisting{generated/logic__quantfmla4.ml}
217

MARCHE Claude's avatar
MARCHE Claude committed
218 219
\section{Building Theories}

220 221 222
We illustrate now how one can build theories. Building a theory must
be done by a sequence of calls:
\begin{itemize}
223
\item creating a theory ``under construction'', of type \verb|Theory.theory_uc|;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
224
\item adding declarations, one at a time;
225 226 227
\item closing the theory under construction, obtaining something of type \verb|Theory.theory|.
\end{itemize}

228
Creation of a theory named \verb|My_theory| is done by
229
\lstinputlisting{generated/logic__buildth1.ml}
230
First let us add formula 1 above as a goal:
231
\lstinputlisting{generated/logic__buildth2.ml}
232 233 234 235 236
Note that we reused the goal identifier \verb|goal_id1| that we
already defined to create task 1 above.

Adding formula 2 needs to add the declarations of predicate variables A
and B first:
237
\lstinputlisting{generated/logic__buildth3.ml}
238 239 240 241 242 243

Adding formula 3 is a bit more complex since it uses integers, thus it
requires to ``use'' the theory \verb|int.Int|. Using a theory is
indeed not a primitive operation in the API: it must be done by a
combination of an ``export'' and the creation of a namespace. We
provide a helper function for that:
244
\lstinputlisting{generated/logic__buildth4.ml}
245
Addition of formula 3 is then
246
\lstinputlisting{generated/logic__buildth5.ml}
247 248

Addition of goal 4 is nothing more complex:
249
\lstinputlisting{generated/logic__buildth6.ml}
250 251

Finally, we close our theory under construction as follows.
252
\lstinputlisting{generated/logic__buildth7.ml}
253

254
We can inspect what we did by printing that theory:
255
\lstinputlisting{generated/logic__printtheory.ml}
256 257
which outputs
\begin{verbatim}
258 259
my new theory is as follows:

260 261
theory My_theory
  (* use BuiltIn *)
262

263
  goal goal1 : true \/ false
264

265
  predicate A
266

267
  predicate B
268

269
  goal goal2 : A /\ B -> A
270

271
  (* use int.Int *)
272

273
  goal goal3 : (2 + 2) = 4
274

275 276 277
  goal goal4 : forall x:int. (x * x) >= 0
end
\end{verbatim}
278 279 280

From a theory, one can compute at once all the proof tasks it contains
as follows:
281
\lstinputlisting{generated/logic__splittheory.ml}
282 283
Note that the tasks are returned in reverse order, so we reverse the
list above.
284 285

We can check our generated tasks by printing them:
286
\lstinputlisting{generated/logic__printalltasks.ml}
287 288

One can run provers on those tasks exactly as we did above.
289

290
\section{Operations on Terms and Formulas, Transformations}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
291

292
The following code illustrates a simple recursive functions of
293
formulas. It explores the formula and when a negation is found, it
294 295
tries to push it down below a conjunction, a disjunction or a
quantifier.
296
\lstinputlisting{generated/transform__negate.ml}
297

298
The following illustrates how to turn such an OCaml function into a
Sylvain Dailler's avatar
Sylvain Dailler committed
299
transformation in the sense of the Why3 API. Moreover, it registers that
300
transformation to make it available for example in Why3 IDE.
301
\lstinputlisting{generated/transform__register.ml}
302

303 304
The directory \verb|src/transform| contains the code for the many
transformations that are already available in Why3.
MARCHE Claude's avatar
MARCHE Claude committed
305

306
\section{Proof Sessions}
307

308 309 310
See the example \verb|examples/use_api/create_session.ml| of the
distribution for an illustration on how to manipulate proof sessions
from an OCaml program.
311

312
\section{ML Programs}
MARCHE Claude's avatar
MARCHE Claude committed
313

314 315 316 317 318 319 320 321 322 323 324
The simplest way to build \whyml programs from OCaml is to build
untyped syntax trees for such programs, and then
call the \why typing procedure to build typed declarations.

The examples of this section are available in the file
\verb|examples/use_api/mlw_tree.ml| of the distribution.

The first step is to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}, and open the OCaml module
\verb|Ptree| which contains most of the OCaml functions we need in
this section.
325
\lstinputlisting{generated/mlw_tree__buildenv.ml}
326 327 328 329 330

To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following
declarations, that first introduces a pseudo ``file'' to hold the
module, then the module itself called \verb|Program|.
331
\lstinputlisting{generated/mlw_tree__openmodule.ml}
332 333
Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without
Sylvain Dailler's avatar
Sylvain Dailler committed
334
any attributes nor any location.
335 336 337 338 339

To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally
imports \verb|int.Int|.
340
\lstinputlisting{generated/mlw_tree__useimport.ml}
341 342

We want now to build a program equivalent to the following code in concrete Why3 syntax.
343
\lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}
344 345

The OCaml code that programmatically build this Why3 function is as follows.
346
\lstinputlisting{generated/mlw_tree__code1.ml}
347 348
This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}.
\begin{figure}[t]
349
  \lstinputlisting{generated/mlw_tree__helper1.ml}
350 351 352 353 354
  \caption{Helper functions for building WhyML programs}
  \label{fig:helpers}
\end{figure}

We want now to build a program equivalent to the following code in concrete Why3 syntax.
355
\lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}
356
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
357
\lstinputlisting{generated/mlw_tree__code2.ml}
358 359

The next example makes use of arrays.
360
\lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}
361
The corresponding OCaml code is as follows
362
\lstinputlisting{generated/mlw_tree__code3.ml}
363 364 365 366

Having declared all the programs we wanted to write, we can now close
the module and the file, and get as a result the set of modules of our
file, under the form of a map of module names to modules.
367
\lstinputlisting{generated/mlw_tree__closemodule.ml}
368 369

We can then construct the proofs tasks for our module, and then try to
Sylvain Dailler's avatar
Sylvain Dailler committed
370
call the Alt-Ergo prover. The rest of that code is using OCaml
371
functions that were already introduced before.
372
\lstinputlisting{generated/mlw_tree__checkingvcs.ml}
373

MARCHE Claude's avatar
doc  
MARCHE Claude committed
374 375 376 377 378
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: