api.tex 12 KB
Newer Older
1
\chapter{The \why\ Application Programming Interface}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:api}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
3

MARCHE Claude's avatar
MARCHE Claude committed
4
This chapter is a tutorial for the users who wants to link their own
5
OCaml code with the \why\ library. We progressively introduce the way
MARCHE Claude's avatar
MARCHE Claude committed
6
7
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
MARCHE Claude's avatar
MARCHE Claude committed
8
9
tasks. The complete documentation for API calls is given 
[TODO in Chapter~ref{chap:apidoc}.]
10

MARCHE Claude's avatar
MARCHE Claude committed
11
We assume the reader has a fair knowledge of the OCaml
12
language. Notice also that the \why\ library is installed: see
MARCHE Claude's avatar
MARCHE Claude committed
13
Section~\ref{sec:installlib}.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
14

MARCHE Claude's avatar
MARCHE Claude committed
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

\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
a piece of OCaml code for building the formula $true \lor false$.
\begin{verbatim}
(* opening the Why3 library *)
open Why

(* a ground propositional goal: true or false *)
let fmla_true : Term.fmla = Term.f_true
let fmla_false : Term.fmla = Term.f_false
let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false
\end{verbatim}
As one can guess, the type \texttt{fmla} is the type of formulas in
the library.

Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers.
\begin{verbatim}
(* printing the formula *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
\end{verbatim}

Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using
\begin{verbatim}
ocamlc str.cma unix.cma nums.cma dynlink.cma \
        -I +ocamlgraph -I +why3 graph.cma why.cma f.ml -o f
\end{verbatim}
Running the generated executable \texttt{f} results in the following output.
\begin{verbatim}
formula 1 is: true or false
\end{verbatim}

Let's now build a formula with propositional variables: $A \land B
\rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows.
\begin{verbatim}
let prop_var_A : Term.lsymbol = 
  Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol = 
  Term.create_psymbol (Ident.id_fresh "B") []
\end{verbatim}
The type \texttt{lsymbol} is the type of logic symbols. 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.
\begin{verbatim}
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla = 
  Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
\end{verbatim}

As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A and B -> A
\end{verbatim}
75
Notice that the concrete syntax of \why\ forbids predicate identifiers
76
77
78
79
80
81
82
83
84
85
86
87
88
to start with a capital letter. This constraint does not exist when
building those directly using library calls.

\section{Buildings Tasks}

Let's see how we can call a prover to prove a formula. As said in
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
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true and
false$ above, this is done as follows.
\begin{verbatim}
let task1 : Task.task = None (* empty task *)
89
90
91
92
let goal_id1 : Decl.prsymbol = 
  Decl.create_prsymbol (Ident.id_fresh "goal1") 
let task1 : Task.task = 
  Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
93
94
95
96
\end{verbatim}
To make the formula a goal, we must give a name to it, here "goal1". A
goal name has type \texttt{prsymbol}, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete
97
syntax of \why\ requires these symbol to be capitalized, but it is not
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
mandatory when using the library. The second argument of
\texttt{add\_prop\_decl} is the kind of the proposition:
\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}.


Once such a task is built, it can be printed.
\begin{verbatim}
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
\end{verbatim}

The task for our second formula is a bit more complex to build, because the variables A and B must be add as logic declaration in the task.
\begin{verbatim}
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None] 
let task2 = Task.add_logic_decl task2 [prop_var_B, None] 
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") 
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 is:@\n%a@]@." Pretty.print_task task2
\end{verbatim}
The argument \texttt{None} is the declarations of logic symbols means
that they do not have any definition.

Execution of our OCaml program now outputs:
\begin{verbatim}
task 1 is:
theory Task
  goal Goal1 : true or false
end

task 2 is:
theory Task
  logic A
  
  logic B
  
  goal Goal2 : A and B -> A
end
\end{verbatim}

\section{Calling External Provers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
140

141
142
143
144
145
146
147
148
149
150
151
152
153
154
To call an external prover, we need to access the Why configuration
file \texttt{.whyrc}, as it was build using the \texttt{why3config}
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.
\begin{verbatim}
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Util.Mstr.t = 
  Whyconf.get_provers config
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
155
The type \texttt{'a Util.Mstr.t} is a map indexed by strings. This map
156
can provide the set of existing provers. In the following, we directly
MARCHE Claude's avatar
MARCHE Claude committed
157
158
attempt to access the prover Alt-Ergo, which is known to be identified
with id \texttt{"alt-ergo"}.
159
160
161
162
163
164
165
166
167
\begin{verbatim}
(* the [prover alt-ergo] section of the config file *)
let alt_ergo : Whyconf.config_prover = 
  try
    Util.Mstr.find "alt-ergo" provers 
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
    exit 0
\end{verbatim}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
168

MARCHE Claude's avatar
MARCHE Claude committed
169
170
171
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.
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
\begin{verbatim}
(* builds the environment from the [loadpath] *)
let env : Env.env = 
  Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) 
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver = 
  Driver.load_driver env alt_ergo.Whyconf.driver
\end{verbatim}

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
termination. Here is a simple way to proceed
\begin{verbatim}
(* call Alt-Ergo *)
let result1 : Call_provers.prover_result = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task1 () ()
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
  Call_provers.print_prover_result result1
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
193
194
195
196
197
198
This way to call a prover is in general to naive, since it may never
return if the prover runs without time limit. The function
\texttt{prove\_task} has two optional parameters: \texttt{timelimit}
is the maximum allowed running time in seconds, and \texttt{memlimit}
is the maximum allowed memory in megabytes.  The type
\texttt{prover\_result} is a record with three fields:
199
200
\begin{itemize}
\item \texttt{pr\_answer}: the prover answer, detailed below.
MARCHE Claude's avatar
MARCHE Claude committed
201
202
\item \texttt{pr\_output}: the output of the prover, i.e. both
  standard output and the standard error of the process
203
204
205
206
207
208
\item \texttt{pr\_time} : the time taken by the prover, in seconds
\end{itemize}
a \texttt{pr\_answer} is a sum of several kind of answers:
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover.
\item \texttt{Invalid}: the task is invalid.
MARCHE Claude's avatar
MARCHE Claude committed
209
210
211
212
213
214
215
216
217
218
\item \texttt{Timeout}: the task timeouts, i.e. it takes more time
  than specified.
\item \texttt{Unknown} $msg$: the prover can't determine if the task
  is valid. the string parameter $msg$ indicates some extra
  information.
\item \texttt{Failure} $msg$: the prover reports a failure, i.e. it
  was unable to read correctly its input task.
\item \texttt{HighFailure}: an error occurred while trying to call the
  prover, or the prover answer was not understood (i.e. none of the
  given regexps in the driver file match the output of the prover).
219
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
220
221
Here is thus another way of calling the Alt-Ergo prover, on our second
task.
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
\begin{verbatim}
let result2 : Call_provers.prover_result = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    ~timelimit:10
    alt_ergo_driver task2 () ()

let () = 
  printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
    Call_provers.print_prover_answer 
    result1.Call_provers.pr_answer
    result1.Call_provers.pr_time
\end{verbatim}
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
241
242
243
244
245

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

246
Here is the way we build the formula $2+2=4$. The main difficult is to
247
248
access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
MARCHE Claude's avatar
MARCHE Claude committed
249
Chap~\ref{chap:library}).
250
251
252
253
254
255
256
257
258
259
260
261
262
263
\begin{verbatim}
let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4")
let int_theory : Theory.theory = 
  Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = 
  Term.t_app_infer plus_symbol [two;two] 
let fmla3 : Term.fmla = Term.f_equ two_plus_two four
\end{verbatim}
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
264
term. One could also provide the expected type as follows.
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
\begin{verbatim}
let two_plus_two : Term.term = 
  Term.t_app plus_symbol [two;two] Ty.ty_int
\end{verbatim}

When building a task with this formula, we need to declare that we use the Int theory, as follows.
\begin{verbatim}
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") 
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
\end{verbatim}

\section{Building Quantified Formulas}

To illustrate how to build quantified formulas, let's build $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from the int theory.
\begin{verbatim}
let zero : Term.term = Term.t_const (Term.ConstInt "0")
let mult_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
\end{verbatim}
The next step is to introduce the variable $x$ with the type int.
\begin{verbatim}
let var_x : Term.vsymbol = 
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
\end{verbatim}
The formula $x*x \geq 0$ is obtained similarly as the previous example.
\begin{verbatim}
let x : Term.term = Term.t_var var_x
let x_times_x : Term.term = 
  Term.t_app_infer mult_symbol [x;x] 
let fmla4_aux : Term.fmla = 
  Term.f_app ge_symbol [x_times_x;zero]
\end{verbatim}
To quantify on $x$, it is mandatory to first build an intermediate
value of type \texttt{fmla\_quant}.
\begin{verbatim}
let fmla4_quant : Term.fmla_quant = 
  Term.f_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.fmla =
  Term.f_forall fmla4_quant
\end{verbatim}
The second argument of \texttt{f\_close\_quant} is a list of triggers.

MARCHE Claude's avatar
MARCHE Claude committed
311
312
\section{Building Theories}

MARCHE Claude's avatar
MARCHE Claude committed
313
[TO BE COMPLETED]
314

MARCHE Claude's avatar
doc  
MARCHE Claude committed
315
316
\section{Applying transformations}

MARCHE Claude's avatar
MARCHE Claude committed
317
[TO BE COMPLETED]
318
319
320

\section{Writing new functions on term}

MARCHE Claude's avatar
MARCHE Claude committed
321
322
323
324
325
[TO BE COMPLETED]
% pattern-matching on terms, opening a quantifier



326

MARCHE Claude's avatar
doc  
MARCHE Claude committed
327
328
329
330
331
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: