\chapter{Executing \whyml Programs} \label{chap:exec}\index{whyml@\whyml} %HEVEA\cutname{exec.html} This chapter shows how \whyml code can be executed, either by being interpreted or compiled to some existing programming language. \begin{latexonly} Let us consider the program in Figure~\ref{fig:MaxAndSum} on page~\pageref{fig:MaxAndSum} that computes the maximum and the sum of an array of integers. \end{latexonly} \begin{htmlonly} Let us consider the program of Section~\ref{sec:MaxAndSum} that computes the maximum and the sum of an array of integers. \end{htmlonly} Let us assume it is contained in a file \texttt{maxsum.mlw}. \section{Interpreting \whyml Code} \label{sec:execute} \index{execute@\texttt{execute}}\index{interpretation!of \whyml} \index{testing \whyml code} To test function \texttt{max\_sum}, we can introduce a \whyml test function in module \texttt{MaxAndSum} \begin{whycode} let test () = let n = 10 in let a = make n 0 in a[0] <- 9; a[1] <- 5; a[2] <- 0; a[3] <- 2; a[4] <- 7; a[5] <- 3; a[6] <- 2; a[7] <- 1; a[8] <- 10; a[9] <- 6; max_sum a n \end{whycode} and then we use the \texttt{execute} command to interpret this function, as follows: \begin{verbatim} > why3 execute maxsum.mlw MaxAndSum.test Execution of MaxAndSum.test (): type: (int, int) result: (45, 10) globals: \end{verbatim} We get the expected output, namely the pair \texttt{(45, 10)}. \section{Compiling \whyml to OCaml} \label{sec:extract} \index{OCaml}\index{extraction} \index{extract@\texttt{extract}} An alternative to interpretation is to compile \whyml to OCaml. We do so using the \texttt{extract} command, as follows: \begin{verbatim} > why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml \end{verbatim} The \texttt{extract} command requires the name of a driver, which indicates how theories/modules from the \why standard library are translated to OCaml. Here we assume a 64-bit architecture and thus we pass \texttt{ocaml64}. We also specify an output file using option \verb+-o+, namely \texttt{max\_sum.ml}. After this command, the file \texttt{max\_sum.ml} contains an OCaml code for function \texttt{max\_sum}. To compile it, we create a file \texttt{main.ml} containing a call to \texttt{max\_sum}, \emph{e.g.}, \begin{whycode} let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |] let s, m = Max_sum.max_sum a (Z.of_int 10) let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m) \end{whycode} It is convenient to use \texttt{ocamlbuild} to compile and link both files \texttt{max\_sum.ml} and \texttt{main.ml}: \begin{verbatim} > ocamlbuild -pkg zarith main.native \end{verbatim} Since \why's type \texttt{int} is translated to OCaml arbitrary precision integers using the \texttt{ZArith} library, we have to pass option \texttt{-pkg zarith} to \texttt{ocamlbuild}. In order to get extracted code that uses OCaml's native integers instead, one has to use \why's types for 63-bit integers from libraries \texttt{mach.int.Int63} and \texttt{mach.array.Array63}. \paragraph{Extraction Starting Point.} The \texttt{extract} command accepts three different targets for extraction: a \whyml file, a module, or a symbol (function, type, exception). To extract all the symbols from every module of a file named \texttt{f.mlw}, one should write \begin{verbatim} > why3 extract -D f.mlw \end{verbatim} To extract only the symbols from module \texttt{M} of file \texttt{f.mlw}, one should write \begin{verbatim} > why3 extract -D -L f.M \end{verbatim} To extract only the symbol \texttt{s} (a function, a type, or an exception) from module \texttt{M} of file \texttt{f.mlw}, one should write \begin{verbatim} > why3 extract -D -L f.M.s \end{verbatim} Note the use of~\texttt{-L }, for both extraction of a module and a symbol, in order to state the location of file \texttt{f.mlw}. \paragraph{Options.} The following options can be added to the extraction command line: \begin{description} \item[\texttt{-{}-flat}] performs a flat extraction, \emph{i.e.}, everything is extracted into a single file. This is the default behavior. The \texttt{-o} option should be given the name of a file or, if omitted, the result of extraction is printed to the standard output. \item[\texttt{-{}-modular}] each module is extracted in its own, separated file. The \texttt{-o} option cannot be omitted, and it should be given the name of an existing directory. This directory will be populated with the resulting OCaml files. \item[\texttt{-{}-recursive}] recursively extracts all the dependencies of the chosen entry point. This option is valid for both \texttt{modular} and \texttt{flat} options. \end{description} \paragraph{Examples.} We illustrate different ways of using the \texttt{extract} command through some examples. \begin{latexonly} Consider the program in Figure~\ref{fig:AQueue} on page~\pageref{fig:AQueue}. \end{latexonly} \begin{htmlonly} Consider the program of Section~\ref{sec:AQueue}. \end{htmlonly} If we are only interested in extracting function \texttt{enqueue}, we can proceed as follows: \begin{verbatim} > why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml \end{verbatim} Here we assume that file \texttt{aqueue.mlw} contains this program, and that we invoke \texttt{extract} from the directory where this file is stored. File \texttt{aqueue.ml} now contains the following OCaml code: \begin{whycode} let enqueue (x: 'a) (q: 'a queue) : 'a queue = create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1")) \end{whycode} Choosing a function symbol as the entry point of extraction allows us to focus only on specific parts of the program. However, the generated code cannot be type-checked by the OCaml compiler, as it depends on function \texttt{create} and on type \texttt{'a queue}, whose definitions are not given. In order to obtain a \emph{complete} OCaml implementation, we can perform a recursive extraction: \begin{verbatim} > why3 extract --recursive -D ocaml64 -L . \ aqueue.AmortizedQueue.enqueue -o aqueue.ml \end{verbatim} This updates the contents of file \texttt{aqueue.ml} as follows: %\begin{figure} \begin{whycode} type 'a queue = { front: 'a list; lenf: Z.t; rear: 'a list; lenr: Z.t; } let create (f: 'a list) (lf: Z.t) (r: 'a list) (lr: Z.t) : 'a queue = if Z.geq lf lr then { front = f; lenf = lf; rear = r; lenr = lr } else let f1 = List.append f (List.rev r) in { front = f1; lenf = Z.add lf lr; rear = []; lenr = (Z.of_string "0") } let enqueue (x: 'a) (q: 'a queue) : 'a queue = create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1")) \end{whycode} This new version of the code is now accepted by the OCaml compiler (provided the \texttt{ZArith} library is available, as above). \paragraph{Custom Extraction Drivers.} Several OCaml drivers can be specified on the command line, using option \texttt{-D} several times. In particular, one can provide a custom driver to map some symbols of a Why3 development to existing OCaml code. Suppose for instance we have a file \texttt{file.mlw} containing a proof parameterized with some type \texttt{elt} and some binary function \texttt{f}: \begin{whycode} module M type elt val f (x y: elt) : elt let double (x: elt) : elt = f x x ... \end{whycode} When it comes to extract this module to OCaml, we may want to instantiate type \texttt{elt} with OCaml's type \texttt{int} and function \texttt{f} with OCaml's addition. For this purpose, we provide the following in a file \texttt{mydriver.drv}: \begin{whycode} module file.M syntax type elt "int" syntax val f "%1 + %2" end \end{whycode} OCaml fragments to be substituted for Why3 symbols are given as arbitrary strings, where \verb+%1+, \verb+%2+, etc., will be replaced with actual arguments. Here is the extraction command line and its output: \begin{verbatim} > why3 extract -D ocaml64 -D mydriver.drv -L . file.M let double (x: int) : int = x + x ... \end{verbatim} When using such custom drivers, it is not possible to pass Why3 file names on the command line; one has to specify module names to be extracted, as done above. %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: