\chapter{The \why API} \label{chap:api}\index{API} This chapter is a tutorial for the users who want to link their own OCaml code with the \why 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 tasks. The complete documentation for API calls is given at URL~\url{http://why3.lri.fr/api/}. We assume the reader has a fair knowledge of the OCaml language. Notice that the \why library must be installed, see Section~\ref{sec:installlib}. The OCaml code given below is available in the source distribution as \url{examples/use_api.ml}. \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 Why3 (* a ground propositional goal: true or false *) 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 \end{verbatim} 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}. Such a formula can be printed using the module \texttt{Pretty} providing pretty-printers. \begin{verbatim} (* printing it *) open Format let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term 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 \/ 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 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. \begin{verbatim} 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 \end{verbatim} As expected, the output is as follows. \begin{verbatim} formula 2 is: A /\ B -> A \end{verbatim} 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. \section{Building 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 \lor false$ above, this is done as follows. \begin{verbatim} let task1 : Task.task = None (* empty task *) 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 \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 \why requires these symbols 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} (notice, however, that lemmas are not allowed in tasks and can only be used in theories). Once 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 added as abstract (i.e.~not defined) propositional symbols in the task. \begin{verbatim} (* task for formula 2 *) let task2 = None let task2 = Task.add_param_decl task2 prop_var_A let task2 = Task.add_param_decl task2 prop_var_B 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} Execution of our OCaml program now outputs: \begin{verbatim} task 1 is: theory Task goal Goal1 : true \/ false end task 2 is: theory Task predicate A predicate B goal Goal2 : A /\ B -> A end \end{verbatim} \section{Calling External Provers} To call an external prover, we need to access the Why configuration file \texttt{why3.conf}, as it was built 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 Whyconf.Mprover.t = Whyconf.get_provers config \end{verbatim} 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 attempt 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 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 with Not_found -> eprintf "Prover alt-ergo not installed or not configured@."; exit 0 \end{verbatim} 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 (Whyconf.loadpath main) (* loading the Alt-Ergo driver *) let alt_ergo_driver : Driver.driver = 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 \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} (* calls Alt-Ergo *) let result1 : Call_provers.prover_result = Call_provers.wait_on_call (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 too 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: \begin{itemize} \item \texttt{pr\_answer}: the prover answer, explained below; \item \texttt{pr\_output}: the output of the prover, i.e. both standard output and the standard error of the process (a redirection in \texttt{why3.conf} is required); \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 prover exceeds the time or memory limit. \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 regular expressions in the driver file matches 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 = Call_provers.wait_on_call (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} An important feature of the functions for building terms and formulas is that they statically guarantee that only well-typed terms can be constructed. Here is the way we build the formula $2+2=4$. The main difficulty is to access the internal identifier for addition: it must be retrieved from the standard theory \texttt{Int} of the file \texttt{int.why} (see Chap~\ref{chap:library}). \begin{verbatim} let two : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "2")) let four : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "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.term = Term.t_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 type as follows. \begin{verbatim} let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int \end{verbatim} When building a task with this formula, we need to declare that we use theory \texttt{Int}: \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 us consider the formula $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from \texttt{Int}. \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 as in 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.term = Term.ps_app ge_symbol [x_times_x;zero] \end{verbatim} To quantify on $x$, we use the appropriate smart constructor as follows. \begin{verbatim} let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux \end{verbatim} \section{Building Theories} [TO BE COMPLETED] \section{Applying transformations} [TO BE COMPLETED] \section{Writing new functions on term} [TO BE COMPLETED] % pattern-matching on terms, opening a quantifier %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: