MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

api.tex 13.4 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
\chapter{The \why API}
2
\label{chap:api}\index{API}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
3

4
This chapter is a tutorial for the users who want to link their own
MARCHE Claude's avatar
MARCHE Claude committed
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
8
tasks. The complete documentation for API calls is given
9
at URL~\url{http://why3.lri.fr/api/}.
10

MARCHE Claude's avatar
MARCHE Claude committed
11
We assume the reader has a fair knowledge of the OCaml
MARCHE Claude's avatar
MARCHE Claude committed
12
language. Notice that the \why library must be installed, see
13
14
Section~\ref{sec:installlib}. The OCaml code given below is available in
the source distribution as \url{examples/use_api.ml}.
MARCHE Claude's avatar
doc    
MARCHE Claude committed
15

MARCHE Claude's avatar
MARCHE Claude committed
16
17
18
19
20
21
22
23

\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 *)
24
open Why3
MARCHE Claude's avatar
MARCHE Claude committed
25
26

(* a ground propositional goal: true or false *)
Andrei Paskevich's avatar
Andrei Paskevich committed
27
28
29
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false
MARCHE Claude's avatar
MARCHE Claude committed
30
\end{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
31
32
33
34
35
36
37
The library uses the common type \texttt{term} both for terms
(i.e.~expressions that produce a value of some particular type)
and formulas (i.e.~boolean-valued expressions).
% 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
38
39
40
41

Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers.
\begin{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
42
(* printing it *)
MARCHE Claude's avatar
MARCHE Claude committed
43
open Format
Andrei Paskevich's avatar
Andrei Paskevich committed
44
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
MARCHE Claude's avatar
MARCHE Claude committed
45
46
47
48
49
50
51
52
53
54
\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}
55
formula 1 is: true \/ false
MARCHE Claude's avatar
MARCHE Claude committed
56
57
58
59
60
61
\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}
62
let prop_var_A : Term.lsymbol =
MARCHE Claude's avatar
MARCHE Claude committed
63
  Term.create_psymbol (Ident.id_fresh "A") []
64
let prop_var_B : Term.lsymbol =
MARCHE Claude's avatar
MARCHE Claude committed
65
66
  Term.create_psymbol (Ident.id_fresh "B") []
\end{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
67
68
69
70
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.
MARCHE Claude's avatar
MARCHE Claude committed
71
\begin{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
72
73
74
75
76
let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term =
  Term.t_implies (Term.t_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
MARCHE Claude's avatar
MARCHE Claude committed
77
78
79
80
\end{verbatim}

As expected, the output is as follows.
\begin{verbatim}
81
formula 2 is: A /\ B -> A
MARCHE Claude's avatar
MARCHE Claude committed
82
\end{verbatim}
Andrei Paskevich's avatar
Andrei Paskevich committed
83
84
85
86
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.
87

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
88
\section{Building Tasks}
89
90
91
92
93

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
94
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true \lor
95
96
97
false$ above, this is done as follows.
\begin{verbatim}
let task1 : Task.task = None (* empty task *)
98
99
100
let goal_id1 : Decl.prsymbol =
  Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task =
101
  Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
102
103
104
105
\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
MARCHE Claude's avatar
MARCHE Claude committed
106
syntax of \why requires these symbols to be capitalized, but it is not
107
108
mandatory when using the library. The second argument of
\texttt{add\_prop\_decl} is the kind of the proposition:
109
110
111
\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}
(notice, however, that lemmas are not allowed in tasks
and can only be used in theories).
112
113


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

120
The task for our second formula is a bit more complex to build, because
Andrei Paskevich's avatar
Andrei Paskevich committed
121
122
the variables A and B must be added as abstract (i.e.~not defined)
propositional symbols in the task.
123
124
125
\begin{verbatim}
(* task for formula 2 *)
let task2 = None
Andrei Paskevich's avatar
Andrei Paskevich committed
126
127
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
128
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
129
130
131
132
133
134
135
136
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}

Execution of our OCaml program now outputs:
\begin{verbatim}
task 1 is:
theory Task
137
  goal Goal1 : true \/ false
138
139
140
141
end

task 2 is:
theory Task
142
  predicate A
143

144
  predicate B
145

146
  goal Goal2 : A /\ B -> A
147
148
149
150
end
\end{verbatim}

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

152
To call an external prover, we need to access the Why configuration
153
file \texttt{why3.conf}, as it was built using the \texttt{why3config}
154
155
156
157
158
159
160
161
162
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 *)
163
let provers : Whyconf.config_prover Whyconf.Mprover.t =
164
165
  Whyconf.get_provers config
\end{verbatim}
166
167
168
169
170
171
172
173
174
175
176
177
178
179
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
provers is a record with a name, a version and an alternative description
(if someone want to compare different command line options of the same
provers for example). It's definition is in the module
\texttt{Whyconf} :
\begin{verbatim}
type prover =
    { prover_name : string; (* "Alt-Ergo" *)
      prover_version : string; (* "2.95" *)
      prover_altern : string; (* "special" *)
    }
\end{verbatim}
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
MARCHE Claude's avatar
MARCHE Claude committed
180
181
attempt to access the prover Alt-Ergo, which is known to be identified
with id \texttt{"alt-ergo"}.
182
183
\begin{verbatim}
(* the [prover alt-ergo] section of the config file *)
184
let alt_ergo : Whyconf.config_prover =
185
  try
186
187
188
189
190
191
192
193
194
195
196
197
198
    Whyconf.prover_by_id config "alt-ergo"
  with Whyconf.ProverNotFound _ ->
    eprintf "Prover alt-ergo not installed or not configured@.";
    exit 0
\end{verbatim}
We could also get a specific version with :
\begin{verbatim}
let alt_ergo : Whyconf.config_prover =
  try
    let prover = {Whyconf.prover_name = "Alt-Ergo";
                  prover_version = "0.92.3";
                  prover_altern = ""} in
    Whyconf.Mprover.find prover provers
199
200
201
202
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
    exit 0
\end{verbatim}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
203

MARCHE Claude's avatar
MARCHE Claude committed
204
205
206
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.
207
208
\begin{verbatim}
(* builds the environment from the [loadpath] *)
209
let env : Env.env =
210
  Env.create_env (Whyconf.loadpath main)
211
(* loading the Alt-Ergo driver *)
212
let alt_ergo_driver : Driver.driver =
213
214
215
216
217
218
  try
    Driver.load_driver env alt_ergo.Whyconf.driver
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1
219
220
221
222
\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
223
termination. Here is a simple way to proceed:
224
\begin{verbatim}
225
226
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
227
228
229
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task1 ()) ()
230
(* prints Alt-Ergo answer *)
231
let () = printf "@[On task 1, alt-ergo answers %a@]@."
232
233
  Call_provers.print_prover_result result1
\end{verbatim}
234
This way to call a prover is in general too naive, since it may never
MARCHE Claude's avatar
MARCHE Claude committed
235
236
237
238
239
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:
240
\begin{itemize}
241
\item \texttt{pr\_answer}: the prover answer, explained below;
MARCHE Claude's avatar
MARCHE Claude committed
242
243
\item \texttt{pr\_output}: the output of the prover, i.e. both
  standard output and the standard error of the process
244
  (a redirection in \texttt{why3.conf} is required);
245
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
246
\end{itemize}
247
A \texttt{pr\_answer} is a sum of several kind of answers:
248
249
250
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover.
\item \texttt{Invalid}: the task is invalid.
251
\item \texttt{Timeout}: the prover exceeds the time or memory limit.
MARCHE Claude's avatar
MARCHE Claude committed
252
\item \texttt{Unknown} $msg$: the prover can't determine if the task
253
  is valid; the string parameter $msg$ indicates some extra
MARCHE Claude's avatar
MARCHE Claude committed
254
  information.
255
\item \texttt{Failure} $msg$: the prover reports a failure, i.e.~it
MARCHE Claude's avatar
MARCHE Claude committed
256
257
  was unable to read correctly its input task.
\item \texttt{HighFailure}: an error occurred while trying to call the
258
259
260
  prover, or the prover answer was not understood (i.e.~none of the
  given regular expressions in the driver file matches the output
  of the prover).
261
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
262
263
Here is thus another way of calling the Alt-Ergo prover, on our second
task.
264
\begin{verbatim}
265
let result2 : Call_provers.prover_result =
266
267
   Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
268
    ~timelimit:10
269
    alt_ergo_driver task2 ()) ()
270

271
let () =
272
  printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
273
    Call_provers.print_prover_answer
274
275
276
277
278
279
280
281
282
283
    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
284
285
286
287
288

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

289
Here is the way we build the formula $2+2=4$. The main difficulty is to
290
291
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
292
Chap~\ref{chap:library}).
293
\begin{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
294
295
let two : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "2"))
let four : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "4"))
296
let int_theory : Theory.theory =
297
  Env.find_theory env ["int"] "Int"
298
let plus_symbol : Term.lsymbol =
299
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
300
301
let two_plus_two : Term.term =
  Term.t_app_infer plus_symbol [two;two]
Andrei Paskevich's avatar
Andrei Paskevich committed
302
let fmla3 : Term.term = Term.t_equ two_plus_two four
303
304
305
306
\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
307
term. One could also provide the expected type as follows.
308
\begin{verbatim}
309
let two_plus_two : Term.term =
Andrei Paskevich's avatar
Andrei Paskevich committed
310
  Term.fs_app plus_symbol [two;two] Ty.ty_int
311
312
\end{verbatim}

313
314
When building a task with this formula, we need to declare that we use
theory \texttt{Int}:
315
316
317
\begin{verbatim}
let task3 = None
let task3 = Task.use_export task3 int_theory
318
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
319
320
321
322
323
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
\end{verbatim}

\section{Building Quantified Formulas}

324
325
326
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}.
327
328
\begin{verbatim}
let zero : Term.term = Term.t_const (Term.ConstInt "0")
329
let mult_symbol : Term.lsymbol =
330
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
331
let ge_symbol : Term.lsymbol =
332
333
334
335
  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}
336
let var_x : Term.vsymbol =
337
338
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
\end{verbatim}
339
The formula $x*x \geq 0$ is obtained as in the previous example.
340
341
\begin{verbatim}
let x : Term.term = Term.t_var var_x
342
let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]
Andrei Paskevich's avatar
Andrei Paskevich committed
343
let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero]
344
\end{verbatim}
345
To quantify on $x$, we use the appropriate smart constructor as follows.
346
\begin{verbatim}
347
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
348
349
\end{verbatim}

MARCHE Claude's avatar
MARCHE Claude committed
350
351
\section{Building Theories}

MARCHE Claude's avatar
MARCHE Claude committed
352
[TO BE COMPLETED]
353

MARCHE Claude's avatar
doc    
MARCHE Claude committed
354
355
\section{Applying transformations}

MARCHE Claude's avatar
MARCHE Claude committed
356
[TO BE COMPLETED]
357
358
359

\section{Writing new functions on term}

MARCHE Claude's avatar
MARCHE Claude committed
360
361
362
363
364
[TO BE COMPLETED]
% pattern-matching on terms, opening a quantifier



365

MARCHE Claude's avatar
doc    
MARCHE Claude committed
366
367
368
369
370
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: