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

api.tex 13.4 KB
 MARCHE Claude committed Jul 02, 2011 1 \chapter{The \why API}  Jean-Christophe Filliâtre committed Aug 21, 2012 2 \label{chap:api}\index{API}  MARCHE Claude committed Sep 06, 2010 3   Andrei Paskevich committed Dec 20, 2010 4 This chapter is a tutorial for the users who want to link their own  MARCHE Claude committed Jul 02, 2011 5 OCaml code with the \why library. We progressively introduce the way  MARCHE Claude committed Dec 08, 2010 6 7 one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on  Andrei Paskevich committed Dec 20, 2010 8 tasks. The complete documentation for API calls is given  MARCHE Claude committed Jul 02, 2011 9 at URL~\url{http://why3.lri.fr/api/}.  MARCHE Claude committed Dec 08, 2010 10   MARCHE Claude committed Dec 16, 2010 11 We assume the reader has a fair knowledge of the OCaml  MARCHE Claude committed Jul 02, 2011 12 language. Notice that the \why library must be installed, see  MARCHE Claude committed Jul 02, 2011 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 committed Sep 06, 2010 15   MARCHE Claude committed Dec 08, 2010 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 *)  Andrei Paskevich committed Jul 02, 2011 24 open Why3  MARCHE Claude committed Dec 08, 2010 25 26  (* a ground propositional goal: true or false *)  Andrei Paskevich committed Jun 18, 2011 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 committed Dec 08, 2010 30 \end{verbatim}  Andrei Paskevich committed Jun 18, 2011 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 committed Dec 08, 2010 38 39 40 41  Such a formula can be printed using the module \texttt{Pretty} providing pretty-printers. \begin{verbatim}  Andrei Paskevich committed Jun 18, 2011 42 (* printing it *)  MARCHE Claude committed Dec 08, 2010 43 open Format  Andrei Paskevich committed Jun 18, 2011 44 let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1  MARCHE Claude committed Dec 08, 2010 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}  Andrei Paskevich committed Jun 30, 2011 55 formula 1 is: true \/ false  MARCHE Claude committed Dec 08, 2010 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}  Andrei Paskevich committed Dec 20, 2010 62 let prop_var_A : Term.lsymbol =  MARCHE Claude committed Dec 08, 2010 63  Term.create_psymbol (Ident.id_fresh "A") []  Andrei Paskevich committed Dec 20, 2010 64 let prop_var_B : Term.lsymbol =  MARCHE Claude committed Dec 08, 2010 65 66  Term.create_psymbol (Ident.id_fresh "B") [] \end{verbatim}  Andrei Paskevich committed Jun 18, 2011 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 committed Dec 08, 2010 71 \begin{verbatim}  Andrei Paskevich committed Jun 18, 2011 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 committed Dec 08, 2010 77 78 79 80 \end{verbatim} As expected, the output is as follows. \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 81 formula 2 is: A /\ B -> A  MARCHE Claude committed Dec 08, 2010 82 \end{verbatim}  Andrei Paskevich committed Jul 02, 2011 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.  MARCHE Claude committed Dec 08, 2010 87   MARCHE Claude committed Dec 17, 2010 88 \section{Building Tasks}  MARCHE Claude committed Dec 08, 2010 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  Andrei Paskevich committed Dec 20, 2010 94 \texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true \lor  MARCHE Claude committed Dec 08, 2010 95 96 97 false$ above, this is done as follows. \begin{verbatim} let task1 : Task.task = None (* empty task *)  Andrei Paskevich committed Dec 20, 2010 98 99 100 let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") let task1 : Task.task =  MARCHE Claude committed Dec 08, 2010 101  Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1  MARCHE Claude committed Dec 08, 2010 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 committed Jul 02, 2011 106 syntax of \why requires these symbols to be capitalized, but it is not  MARCHE Claude committed Dec 08, 2010 107 108 mandatory when using the library. The second argument of \texttt{add\_prop\_decl} is the kind of the proposition:  Andrei Paskevich committed Dec 20, 2010 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).  MARCHE Claude committed Dec 08, 2010 112 113   Andrei Paskevich committed Dec 20, 2010 114 Once a task is built, it can be printed.  MARCHE Claude committed Dec 08, 2010 115 116 117 118 119 \begin{verbatim} (* printing the task *) let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1 \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 120 The task for our second formula is a bit more complex to build, because  Andrei Paskevich committed Mar 18, 2012 121 122 the variables A and B must be added as abstract (i.e.~not defined) propositional symbols in the task.  MARCHE Claude committed Dec 08, 2010 123 124 125 \begin{verbatim} (* task for formula 2 *) let task2 = None  Andrei Paskevich committed Mar 18, 2012 126 127 let task2 = Task.add_param_decl task2 prop_var_A let task2 = Task.add_param_decl task2 prop_var_B  Andrei Paskevich committed Dec 20, 2010 128 let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")  MARCHE Claude committed Dec 08, 2010 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  Andrei Paskevich committed Jun 30, 2011 137  goal Goal1 : true \/ false  MARCHE Claude committed Dec 08, 2010 138 139 140 141 end task 2 is: theory Task  Andrei Paskevich committed Jun 30, 2011 142  predicate A  Andrei Paskevich committed Dec 20, 2010 143   Andrei Paskevich committed Jun 30, 2011 144  predicate B  Andrei Paskevich committed Dec 20, 2010 145   Andrei Paskevich committed Jun 30, 2011 146  goal Goal2 : A /\ B -> A  MARCHE Claude committed Dec 08, 2010 147 148 149 150 end \end{verbatim} \section{Calling External Provers}  MARCHE Claude committed Sep 06, 2010 151   MARCHE Claude committed Dec 08, 2010 152 To call an external prover, we need to access the Why configuration  Andrei Paskevich committed Jul 02, 2011 153 file \texttt{why3.conf}, as it was built using the \texttt{why3config}  MARCHE Claude committed Dec 08, 2010 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 *)  François Bobot committed Jan 25, 2012 163 let provers : Whyconf.config_prover Whyconf.Mprover.t =  MARCHE Claude committed Dec 08, 2010 164 165  Whyconf.get_provers config \end{verbatim}  François Bobot committed Jan 25, 2012 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 committed Dec 16, 2010 180 181 attempt to access the prover Alt-Ergo, which is known to be identified with id \texttt{"alt-ergo"}.  MARCHE Claude committed Dec 08, 2010 182 183 \begin{verbatim} (* the [prover alt-ergo] section of the config file *)  Andrei Paskevich committed Dec 20, 2010 184 let alt_ergo : Whyconf.config_prover =  MARCHE Claude committed Dec 08, 2010 185  try  François Bobot committed Jan 25, 2012 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  MARCHE Claude committed Dec 08, 2010 199 200 201 202  with Not_found -> eprintf "Prover alt-ergo not installed or not configured@."; exit 0 \end{verbatim}  MARCHE Claude committed Sep 06, 2010 203   MARCHE Claude committed Dec 16, 2010 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.  MARCHE Claude committed Dec 08, 2010 207 208 \begin{verbatim} (* builds the environment from the [loadpath] *)  Andrei Paskevich committed Dec 20, 2010 209 let env : Env.env =  Andrei Paskevich committed Sep 30, 2011 210  Env.create_env (Whyconf.loadpath main)  MARCHE Claude committed Dec 08, 2010 211 (* loading the Alt-Ergo driver *)  Andrei Paskevich committed Dec 20, 2010 212 let alt_ergo_driver : Driver.driver =  MARCHE Claude committed Jul 02, 2011 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  MARCHE Claude committed Dec 08, 2010 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  Andrei Paskevich committed Dec 20, 2010 223 termination. Here is a simple way to proceed:  MARCHE Claude committed Dec 08, 2010 224 \begin{verbatim}  Andrei Paskevich committed Dec 20, 2010 225 226 (* calls Alt-Ergo *) let result1 : Call_provers.prover_result =  Jean-Christophe Filliâtre committed Feb 24, 2011 227 228 229  Call_provers.wait_on_call (Driver.prove_task ~command:alt_ergo.Whyconf.command alt_ergo_driver task1 ()) ()  MARCHE Claude committed Dec 08, 2010 230 (* prints Alt-Ergo answer *)  Andrei Paskevich committed Dec 20, 2010 231 let () = printf "@[On task 1, alt-ergo answers %a@]@."  MARCHE Claude committed Dec 08, 2010 232 233  Call_provers.print_prover_result result1 \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 234 This way to call a prover is in general too naive, since it may never  MARCHE Claude committed Dec 16, 2010 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:  MARCHE Claude committed Dec 08, 2010 240 \begin{itemize}  Andrei Paskevich committed Dec 20, 2010 241 \item \texttt{pr\_answer}: the prover answer, explained below;  MARCHE Claude committed Dec 16, 2010 242 243 \item \texttt{pr\_output}: the output of the prover, i.e. both standard output and the standard error of the process  Andrei Paskevich committed Jul 02, 2011 244  (a redirection in \texttt{why3.conf} is required);  Andrei Paskevich committed Dec 20, 2010 245 \item \texttt{pr\_time} : the time taken by the prover, in seconds.  MARCHE Claude committed Dec 08, 2010 246 \end{itemize}  Andrei Paskevich committed Dec 20, 2010 247 A \texttt{pr\_answer} is a sum of several kind of answers:  MARCHE Claude committed Dec 08, 2010 248 249 250 \begin{itemize} \item \texttt{Valid}: the task is valid according to the prover. \item \texttt{Invalid}: the task is invalid.  Andrei Paskevich committed Dec 20, 2010 251 \item \texttt{Timeout}: the prover exceeds the time or memory limit.  MARCHE Claude committed Dec 16, 2010 252 \item \texttt{Unknown} $msg$: the prover can't determine if the task  Andrei Paskevich committed Dec 20, 2010 253  is valid; the string parameter $msg$ indicates some extra  MARCHE Claude committed Dec 16, 2010 254  information.  Andrei Paskevich committed Dec 20, 2010 255 \item \texttt{Failure} $msg$: the prover reports a failure, i.e.~it  MARCHE Claude committed Dec 16, 2010 256 257  was unable to read correctly its input task. \item \texttt{HighFailure}: an error occurred while trying to call the  Andrei Paskevich committed Dec 20, 2010 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).  MARCHE Claude committed Dec 08, 2010 261 \end{itemize}  MARCHE Claude committed Dec 16, 2010 262 263 Here is thus another way of calling the Alt-Ergo prover, on our second task.  MARCHE Claude committed Dec 08, 2010 264 \begin{verbatim}  Andrei Paskevich committed Dec 20, 2010 265 let result2 : Call_provers.prover_result =  Jean-Christophe Filliâtre committed Feb 24, 2011 266 267  Call_provers.wait_on_call (Driver.prove_task ~command:alt_ergo.Whyconf.command  MARCHE Claude committed Dec 08, 2010 268  ~timelimit:10  Jean-Christophe Filliâtre committed Feb 24, 2011 269  alt_ergo_driver task2 ()) ()  MARCHE Claude committed Dec 08, 2010 270   Andrei Paskevich committed Dec 20, 2010 271 let () =  MARCHE Claude committed Dec 08, 2010 272  printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."  Andrei Paskevich committed Dec 20, 2010 273  Call_provers.print_prover_answer  MARCHE Claude committed Dec 08, 2010 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 committed Dec 08, 2010 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.  Andrei Paskevich committed Dec 20, 2010 289 Here is the way we build the formula $2+2=4$. The main difficulty is to  MARCHE Claude committed Dec 09, 2010 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 committed Dec 13, 2010 292 Chap~\ref{chap:library}).  MARCHE Claude committed Dec 08, 2010 293 \begin{verbatim}  MARCHE Claude committed Jun 20, 2012 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"))  Andrei Paskevich committed Dec 20, 2010 296 let int_theory : Theory.theory =  MARCHE Claude committed Dec 08, 2010 297  Env.find_theory env ["int"] "Int"  Andrei Paskevich committed Dec 20, 2010 298 let plus_symbol : Term.lsymbol =  MARCHE Claude committed Dec 08, 2010 299  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]  Andrei Paskevich committed Dec 20, 2010 300 301 let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]  Andrei Paskevich committed Jun 18, 2011 302 let fmla3 : Term.term = Term.t_equ two_plus_two four  MARCHE Claude committed Dec 08, 2010 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  MARCHE Claude committed Dec 09, 2010 307 term. One could also provide the expected type as follows.  MARCHE Claude committed Dec 08, 2010 308 \begin{verbatim}  Andrei Paskevich committed Dec 20, 2010 309 let two_plus_two : Term.term =  Andrei Paskevich committed Jun 18, 2011 310  Term.fs_app plus_symbol [two;two] Ty.ty_int  MARCHE Claude committed Dec 08, 2010 311 312 \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 313 314 When building a task with this formula, we need to declare that we use theory \texttt{Int}:  MARCHE Claude committed Dec 08, 2010 315 316 317 \begin{verbatim} let task3 = None let task3 = Task.use_export task3 int_theory  Andrei Paskevich committed Dec 20, 2010 318 let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")  MARCHE Claude committed Dec 08, 2010 319 320 321 322 323 let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3 \end{verbatim} \section{Building Quantified Formulas}  Andrei Paskevich committed Dec 20, 2010 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}.  MARCHE Claude committed Dec 08, 2010 327 328 \begin{verbatim} let zero : Term.term = Term.t_const (Term.ConstInt "0")  Andrei Paskevich committed Dec 20, 2010 329 let mult_symbol : Term.lsymbol =  MARCHE Claude committed Dec 08, 2010 330  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]  Andrei Paskevich committed Dec 20, 2010 331 let ge_symbol : Term.lsymbol =  MARCHE Claude committed Dec 08, 2010 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}  Andrei Paskevich committed Dec 20, 2010 336 let var_x : Term.vsymbol =  MARCHE Claude committed Dec 08, 2010 337 338  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int \end{verbatim}  Andrei Paskevich committed Dec 20, 2010 339 The formula $x*x \geq 0$ is obtained as in the previous example.  MARCHE Claude committed Dec 08, 2010 340 341 \begin{verbatim} let x : Term.term = Term.t_var var_x  Andrei Paskevich committed Dec 20, 2010 342 let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]  Andrei Paskevich committed Jun 18, 2011 343 let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero]  MARCHE Claude committed Dec 08, 2010 344 \end{verbatim}  MARCHE Claude committed Jul 02, 2011 345 To quantify on $x$, we use the appropriate smart constructor as follows.  Andrei Paskevich committed Dec 20, 2010 346 \begin{verbatim}  MARCHE Claude committed Jul 02, 2011 347 let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux  Andrei Paskevich committed Dec 20, 2010 348 349 \end{verbatim}  MARCHE Claude committed Dec 08, 2010 350 351 \section{Building Theories}  MARCHE Claude committed Dec 15, 2010 352 [TO BE COMPLETED]  MARCHE Claude committed Dec 08, 2010 353   MARCHE Claude committed Sep 06, 2010 354 355 \section{Applying transformations}  MARCHE Claude committed Dec 15, 2010 356 [TO BE COMPLETED]  MARCHE Claude committed Dec 08, 2010 357 358 359  \section{Writing new functions on term}  MARCHE Claude committed Dec 15, 2010 360 361 362 363 364 [TO BE COMPLETED] % pattern-matching on terms, opening a quantifier  MARCHE Claude committed Dec 08, 2010 365   MARCHE Claude committed Sep 06, 2010 366 367 368 369 370 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: