exec.tex 8.12 KB
Newer Older
1 2 3

\chapter{Executing \whyml Programs}
\label{chap:exec}\index{whyml@\whyml}
4
%HEVEA\cutname{exec.html}
5

Guillaume Melquiond's avatar
Guillaume Melquiond committed
6
This chapter shows how \whyml code can be executed, either by being
7 8
interpreted or compiled to some existing programming language.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
9 10
\begin{latexonly}
Let us consider the program in Figure~\ref{fig:MaxAndSum}
11 12
on page~\pageref{fig:MaxAndSum} that computes the maximum and the sum
of an array of integers.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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}
18 19 20
Let us assume it is contained in a file \texttt{maxsum.mlw}.

\section{Interpreting \whyml Code}
21
\label{sec:execute}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
22
\index{execute@\texttt{execute}}\index{interpretation!of \whyml}
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's avatar
Guillaume Melquiond committed
35
and then we use the \texttt{execute} command to interpret this function,
36 37
as follows:
\begin{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38 39 40
> why3 execute maxsum.mlw MaxAndSum.test
Execution of MaxAndSum.test ():
     type: (int, int)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
41
   result: (45, 10)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
42
  globals:
43
\end{verbatim}
44
We get the expected output, namely the pair \texttt{(45, 10)}.
45 46

\section{Compiling \whyml to OCaml}
47
\label{sec:extract}
48
\index{OCaml}\index{extraction}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
49
\index{extract@\texttt{extract}}
50 51

An alternative to interpretation is to compile \whyml to OCaml.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52
We do so using the \texttt{extract} command, as follows:
53
\begin{verbatim}
54
> why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml
55
\end{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
56
The \texttt{extract} command requires the name of a driver, which indicates
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
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}.
63
To compile it, we create a file \texttt{main.ml}
64
containing a call to \texttt{max\_sum}, \emph{e.g.},
65
\begin{whycode}
66
let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |]
67
let s, m = Max_sum.max_sum a (Z.of_int 10)
68
let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m)
69
\end{whycode}
70 71
It is convenient to use \texttt{ocamlbuild} to compile and link both
files \texttt{max\_sum.ml} and \texttt{main.ml}:
72
\begin{verbatim}
73
> ocamlbuild -pkg zarith main.native
74
\end{verbatim}
Mário Pereira's avatar
Mário Pereira committed
75
Since \why's type
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's avatar
Mário Pereira committed
79
uses OCaml's native integers instead, one has to use \why's types for
80 81
63-bit integers from libraries \texttt{mach.int.Int63} and
\texttt{mach.array.Array63}.
82

83
\paragraph{Extraction Starting Point.} The \texttt{extract} command accepts three
Mário Pereira's avatar
Mário Pereira committed
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 <driver> 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 <driver> -L <dir> 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 <driver> -L <dir> f.M.s
\end{verbatim}
Note the use of~\texttt{-L <dir>}, for both extraction of a module and a symbol,
in order to state the location of file \texttt{f.mlw}.

103 104
\paragraph{Options.} The following options can be added to the
extraction command line:
Mário Pereira's avatar
Mário Pereira committed
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}

119 120
\paragraph{Examples.}
We illustrate different ways of using the \texttt{extract} command through some
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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
129
\texttt{enqueue}, we can proceed as follows:
Mário Pereira's avatar
Mário Pereira committed
130
\begin{verbatim}
Mário Pereira's avatar
Mário Pereira committed
131
> why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml
Mário Pereira's avatar
Mário Pereira committed
132
\end{verbatim}
Mário Pereira's avatar
Mário Pereira committed
133
Here we assume that file \texttt{aqueue.mlw} contains this program, and that
Mário Pereira's avatar
Mário Pereira committed
134
we invoke \texttt{extract} from the directory where this file is stored. File
Mário Pereira's avatar
Mário Pereira committed
135
\texttt{aqueue.ml} now contains the following OCaml code:
Mário Pereira's avatar
Mário Pereira committed
136
\begin{whycode}
Mário Pereira's avatar
Mário Pereira committed
137
let enqueue (x: 'a) (q: 'a queue) : 'a queue =
Mário Pereira's avatar
Mário Pereira committed
138 139
  create (q.front) (q.lenf) (x :: (q.rear))
    (Z.add (q.lenr) (Z.of_string "1"))
Mário Pereira's avatar
Mário Pereira committed
140
\end{whycode}
Mário Pereira's avatar
Mário Pereira committed
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's avatar
Mário Pereira committed
145
obtain a \emph{complete} OCaml implementation, we can perform a recursive
Mário Pereira's avatar
Mário Pereira committed
146
extraction:
Mário Pereira's avatar
Mário Pereira committed
147
\begin{verbatim}
148
> why3 extract --recursive -D ocaml64 -L . \
Mário Pereira's avatar
Mário Pereira committed
149
    aqueue.AmortizedQueue.enqueue -o aqueue.ml
Mário Pereira's avatar
Mário Pereira committed
150
\end{verbatim}
Mário Pereira's avatar
Mário Pereira committed
151 152
This updates the contents of file \texttt{aqueue.ml} as follows:
%\begin{figure}
Mário Pereira's avatar
Mário Pereira committed
153
\begin{whycode}
Mário Pereira's avatar
Mário Pereira committed
154 155 156 157 158 159
type 'a queue = {
  front: 'a list;
  lenf: Z.t;
  rear: 'a list;
  lenr: Z.t;
  }
Mário Pereira's avatar
Mário Pereira committed
160

Mário Pereira's avatar
Mário Pereira committed
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's avatar
Mário Pereira committed
168

Mário Pereira's avatar
Mário Pereira committed
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's avatar
Mário Pereira committed
172
\end{whycode}
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's avatar
Mário Pereira committed
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
\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.
212 213 214 215 216 217

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: