api.tex 11.8 KB
 MARCHE Claude committed Sep 06, 2010 1 \chapter{The Why3 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 5 6 7 This chapter is a tutorial for the users who wants to link their own OCaml code with the Why3 library. We progressively introduce the way 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 08, 2010 8 9 10 11 tasks. The complete documentation for API calls is given in Chapter~\ref{chap:apidoc}. We assume the reader has a fair knowledge of the OCaml language.  MARCHE Claude committed Sep 06, 2010 12   MARCHE Claude committed Dec 08, 2010 13 14 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  \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}  MARCHE Claude committed Dec 08, 2010 73 74 75 76 77 78 79 80 81 82 83 84 85 86 Notice that the concrete syntax of Why3 forbids predicate identifiers 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 87 88 89 90 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 91 92 93 94 95 96 97 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 \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 syntax of Why3 requires these symbol to be capitalized, but it is not 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 138   MARCHE Claude committed Dec 08, 2010 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 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} The type \texttt{'a Util.Mstr.t} is a map index by strings. This map can provide the set of existing provers. In the following, we directly attempy to access the prover Alt-Ergo, which is known to be identified with id \texttt{"alt-ergo"}. \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 166   MARCHE Claude committed Dec 08, 2010 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 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. \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} This way to call a prover is in general to naive, since it will never return of the prover runs without time limit. The function \texttt{prove\_task} has two option 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: \begin{itemize} \item \texttt{pr\_answer}: the prover answer, detailed below. \item \texttt{pr\_output}: the output of the prover, i.e. both standard output and the standard error of the process \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. \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). \end{itemize} Here is thus another way of calling the Alt-Ergo prover, on our second task. \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 227 228 229 230 231  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 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 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 Here is the way we build the formula $2+2=4$. The main difficult is to access the internal identifier for addition: it must retrieved from the standard theory \texttt{Int} of the file \texttt{int.why}. \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 term. One could also provide the expected term as follows. \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 296 297 \section{Building Theories}  MARCHE Claude committed Dec 08, 2010 298 299 TODO  MARCHE Claude committed Sep 06, 2010 300 301 \section{Applying transformations}  MARCHE Claude committed Dec 08, 2010 302 303 304 305 306 307 TODO \section{Writing new functions on term} TODO: pattern-matching on terms, opening a quantifier  MARCHE Claude committed Sep 06, 2010 308 309 310 311 312 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: