exec.tex 8.12 KB
 Jean-Christophe Filliatre committed Feb 28, 2014 1 2 3  \chapter{Executing \whyml Programs} \label{chap:exec}\index{whyml@\whyml}  Guillaume Melquiond committed Oct 02, 2017 4 %HEVEA\cutname{exec.html}  Jean-Christophe Filliatre committed Feb 28, 2014 5   Guillaume Melquiond committed Jun 20, 2014 6 This chapter shows how \whyml code can be executed, either by being  Jean-Christophe Filliatre committed Feb 28, 2014 7 8 interpreted or compiled to some existing programming language.  Guillaume Melquiond committed Mar 10, 2014 9 10 \begin{latexonly} Let us consider the program in Figure~\ref{fig:MaxAndSum}  Jean-Christophe Filliatre committed Feb 28, 2014 11 12 on page~\pageref{fig:MaxAndSum} that computes the maximum and the sum of an array of integers.  Guillaume Melquiond committed Mar 10, 2014 13 14 15 16 17 \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}  Jean-Christophe Filliatre committed Feb 28, 2014 18 19 20 Let us assume it is contained in a file \texttt{maxsum.mlw}. \section{Interpreting \whyml Code}  Guillaume Melquiond committed Jun 20, 2014 21 \label{sec:execute}  Guillaume Melquiond committed Jun 03, 2014 22 \index{execute@\texttt{execute}}\index{interpretation!of \whyml}  Jean-Christophe Filliatre committed Feb 28, 2014 23 24 25 26 27 28 29 30 31 32 33 34 \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}  Guillaume Melquiond committed Jun 03, 2014 35 and then we use the \texttt{execute} command to interpret this function,  Jean-Christophe Filliatre committed Feb 28, 2014 36 37 as follows: \begin{verbatim}  Guillaume Melquiond committed Jun 03, 2014 38 39 40 > why3 execute maxsum.mlw MaxAndSum.test Execution of MaxAndSum.test (): type: (int, int)  Guillaume Melquiond committed Jun 20, 2014 41  result: (45, 10)  Guillaume Melquiond committed Jun 03, 2014 42  globals:  Jean-Christophe Filliatre committed Feb 28, 2014 43 \end{verbatim}  Jean-Christophe Filliatre committed Mar 13, 2014 44 We get the expected output, namely the pair \texttt{(45, 10)}.  Jean-Christophe Filliatre committed Feb 28, 2014 45 46  \section{Compiling \whyml to OCaml}  Guillaume Melquiond committed Jun 20, 2014 47 \label{sec:extract}  Jean-Christophe Filliatre committed Feb 28, 2014 48 \index{OCaml}\index{extraction}  Guillaume Melquiond committed Jun 03, 2014 49 \index{extract@\texttt{extract}}  Jean-Christophe Filliatre committed Feb 28, 2014 50 51  An alternative to interpretation is to compile \whyml to OCaml.  Guillaume Melquiond committed Jun 03, 2014 52 We do so using the \texttt{extract} command, as follows:  Jean-Christophe Filliatre committed Feb 28, 2014 53 \begin{verbatim}  Jean-Christophe Filliatre committed May 29, 2017 54 > why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml  Jean-Christophe Filliatre committed Feb 28, 2014 55 \end{verbatim}  Guillaume Melquiond committed Jun 03, 2014 56 The \texttt{extract} command requires the name of a driver, which indicates  Jean-Christophe Filliatre committed Feb 28, 2014 57 58 how theories/modules from the \why standard library are translated to OCaml. Here we assume a 64-bit architecture and thus we pass  Jean-Christophe Filliatre committed May 29, 2017 59 60 61 62 \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}.  Jean-Christophe Filliatre committed Feb 28, 2014 63 To compile it, we create a file \texttt{main.ml}  Jean-Christophe Filliatre committed May 29, 2017 64 containing a call to \texttt{max\_sum}, \emph{e.g.},  Jean-Christophe Filliatre committed Feb 28, 2014 65 \begin{whycode}  Jean-Christophe Filliatre committed May 29, 2017 66 let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |]  Jean-Christophe Filliatre committed May 24, 2018 67 let s, m = Max_sum.max_sum a (Z.of_int 10)  Jean-Christophe Filliatre committed May 29, 2017 68 let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m)  Jean-Christophe Filliatre committed Feb 28, 2014 69 \end{whycode}  Jean-Christophe Filliatre committed May 29, 2017 70 71 It is convenient to use \texttt{ocamlbuild} to compile and link both files \texttt{max\_sum.ml} and \texttt{main.ml}:  Jean-Christophe Filliatre committed Feb 28, 2014 72 \begin{verbatim}  Jean-Christophe Filliatre committed May 29, 2017 73 > ocamlbuild -pkg zarith main.native  Jean-Christophe Filliatre committed Feb 28, 2014 74 \end{verbatim}  Mário Pereira committed May 30, 2017 75 Since \why's type  Jean-Christophe Filliatre committed May 29, 2017 76 77 78 \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  Mário Pereira committed May 30, 2017 79 uses OCaml's native integers instead, one has to use \why's types for  Jean-Christophe Filliatre committed May 29, 2017 80 81 63-bit integers from libraries \texttt{mach.int.Int63} and \texttt{mach.array.Array63}.  Jean-Christophe Filliatre committed Feb 28, 2014 82   Jean-Christophe Filliatre committed May 24, 2018 83 \paragraph{Extraction Starting Point.} The \texttt{extract} command accepts three  Mário Pereira committed May 30, 2017 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 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}.  Jean-Christophe Filliatre committed May 24, 2018 103 104 \paragraph{Options.} The following options can be added to the extraction command line:  Mário Pereira committed May 30, 2017 105 106 107 108 109 110 111 112 113 114 115 116 117 118 \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}  Jean-Christophe Filliatre committed May 24, 2018 119 120 \paragraph{Examples.} We illustrate different ways of using the \texttt{extract} command through some  Guillaume Melquiond committed Jun 23, 2018 121 122 123 124 125 126 127 128 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  Jean-Christophe Filliatre committed May 24, 2018 129 \texttt{enqueue}, we can proceed as follows:  Mário Pereira committed May 30, 2017 130 \begin{verbatim}  Mário Pereira committed May 31, 2017 131 > why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml  Mário Pereira committed May 30, 2017 132 \end{verbatim}  Mário Pereira committed May 31, 2017 133 Here we assume that file \texttt{aqueue.mlw} contains this program, and that  Mário Pereira committed May 30, 2017 134 we invoke \texttt{extract} from the directory where this file is stored. File  Mário Pereira committed May 31, 2017 135 \texttt{aqueue.ml} now contains the following OCaml code:  Mário Pereira committed May 30, 2017 136 \begin{whycode}  Mário Pereira committed May 31, 2017 137 let enqueue (x: 'a) (q: 'a queue) : 'a queue =  Mário Pereira committed Jun 06, 2017 138 139  create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1"))  Mário Pereira committed May 30, 2017 140 \end{whycode}  Mário Pereira committed May 31, 2017 141 142 143 144 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  Mário Pereira committed Jun 06, 2017 145 obtain a \emph{complete} OCaml implementation, we can perform a recursive  Mário Pereira committed May 31, 2017 146 extraction:  Mário Pereira committed May 30, 2017 147 \begin{verbatim}  Jean-Christophe Filliatre committed May 24, 2018 148 > why3 extract --recursive -D ocaml64 -L . \  Mário Pereira committed May 31, 2017 149  aqueue.AmortizedQueue.enqueue -o aqueue.ml  Mário Pereira committed May 30, 2017 150 \end{verbatim}  Mário Pereira committed May 31, 2017 151 152 This updates the contents of file \texttt{aqueue.ml} as follows: %\begin{figure}  Mário Pereira committed May 30, 2017 153 \begin{whycode}  Mário Pereira committed May 31, 2017 154 155 156 157 158 159 type 'a queue = { front: 'a list; lenf: Z.t; rear: 'a list; lenr: Z.t; }  Mário Pereira committed May 30, 2017 160   Mário Pereira committed May 31, 2017 161 162 163 164 165 166 167 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") }  Mário Pereira committed May 30, 2017 168   Mário Pereira committed May 31, 2017 169 170 171 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"))  Mário Pereira committed May 30, 2017 172 \end{whycode}  Jean-Christophe Filliatre committed May 24, 2018 173 174 This new version of the code is now accepted by the OCaml compiler (provided the \texttt{ZArith} library is available, as above).  Mário Pereira committed Jun 06, 2017 175   Jean-Christophe Filliatre committed May 24, 2018 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 \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.  Jean-Christophe Filliatre committed Feb 28, 2014 212 213 214 215 216 217  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: