api.tex 12 KB
 Jean-Christophe Filliâtre committed Dec 17, 2010 1 \chapter{The \why\ Application Programming Interface}  MARCHE Claude committed Sep 08, 2010 2 \label{chap:api}  MARCHE Claude committed Sep 06, 2010 3   MARCHE Claude committed Dec 08, 2010 4 This chapter is a tutorial for the users who wants to link their own  Jean-Christophe Filliâtre committed Dec 17, 2010 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  MARCHE Claude committed Dec 16, 2010 8 9 tasks. The complete documentation for API calls is given [TODO in Chapter~ref{chap:apidoc}.]  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  Jean-Christophe Filliâtre committed Dec 17, 2010 12 language. Notice also that the \why\ library is installed: see  MARCHE Claude committed Dec 16, 2010 13 Section~\ref{sec:installlib}.  MARCHE Claude committed Sep 06, 2010 14   MARCHE Claude committed Dec 08, 2010 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}  Jean-Christophe Filliâtre committed Dec 17, 2010 75 Notice that the concrete syntax of \why\ forbids predicate identifiers  MARCHE Claude committed Dec 08, 2010 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 *)  MARCHE Claude committed Dec 08, 2010 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  MARCHE Claude committed Dec 08, 2010 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  Jean-Christophe Filliâtre committed Dec 17, 2010 97 syntax of \why\ requires these symbol to be capitalized, but it is not  MARCHE Claude committed Dec 08, 2010 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 committed Sep 06, 2010 140   MARCHE Claude committed Dec 08, 2010 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 committed Dec 16, 2010 155 The type \texttt{'a Util.Mstr.t} is a map indexed by strings. This map  MARCHE Claude committed Dec 08, 2010 156 can provide the set of existing provers. In the following, we directly  MARCHE Claude committed Dec 16, 2010 157 158 attempt to access the prover Alt-Ergo, which is known to be identified with id \texttt{"alt-ergo"}.  MARCHE Claude committed Dec 08, 2010 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 committed Sep 06, 2010 168   MARCHE Claude committed Dec 16, 2010 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.  MARCHE Claude committed Dec 08, 2010 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 committed Dec 16, 2010 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:  MARCHE Claude committed Dec 08, 2010 199 200 \begin{itemize} \item \texttt{pr\_answer}: the prover answer, detailed below.  MARCHE Claude committed Dec 16, 2010 201 202 \item \texttt{pr\_output}: the output of the prover, i.e. both standard output and the standard error of the process  MARCHE Claude committed Dec 08, 2010 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 committed Dec 16, 2010 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).  MARCHE Claude committed Dec 08, 2010 219 \end{itemize}  MARCHE Claude committed Dec 16, 2010 220 221 Here is thus another way of calling the Alt-Ergo prover, on our second task.  MARCHE Claude committed Dec 08, 2010 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 committed Dec 08, 2010 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.  MARCHE Claude committed Dec 08, 2010 246 Here is the way we build the formula $2+2=4$. The main difficult is to  MARCHE Claude committed Dec 09, 2010 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 committed Dec 13, 2010 249 Chap~\ref{chap:library}).  MARCHE Claude committed Dec 08, 2010 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  MARCHE Claude committed Dec 09, 2010 264 term. One could also provide the expected type as follows.  MARCHE Claude committed Dec 08, 2010 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 committed Dec 08, 2010 311 312 \section{Building Theories}  MARCHE Claude committed Dec 15, 2010 313 [TO BE COMPLETED]  MARCHE Claude committed Dec 08, 2010 314   MARCHE Claude committed Sep 06, 2010 315 316 \section{Applying transformations}  MARCHE Claude committed Dec 15, 2010 317 [TO BE COMPLETED]  MARCHE Claude committed Dec 08, 2010 318 319 320  \section{Writing new functions on term}  MARCHE Claude committed Dec 15, 2010 321 322 323 324 325 [TO BE COMPLETED] % pattern-matching on terms, opening a quantifier  MARCHE Claude committed Dec 08, 2010 326   MARCHE Claude committed Sep 06, 2010 327 328 329 330 331 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: