
\chapter{Executing \whyml Programs}
\label{chap:exec}\index{whyml@\whyml}

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}
> mkdir dir
> why3 extract -D ocaml64 maxsum.mlw -o dir
\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}. On a 32-bit architecture, we would use
\texttt{ocaml32} instead. Extraction also requires a target directory
to be specified using option \verb+-o+. Here we pass a freshly created
directory \texttt{dir}.

Directory \texttt{dir} is now populated with a bunch of OCaml files,
among which we find a file \texttt{maxsum\_\_MaxAndSum.ml} containing
the OCaml code for functions \texttt{max\_sum} and \texttt{test}.

To compile it, we create a file \texttt{main.ml}
containing a call to \texttt{test}, that is, for example,
\begin{whycode}
  let (s,m) = test () in
  Format.printf "sum=%s, max=%s@."
    (Why3__BigInt.to_string s) (Why3__BigInt.to_string m)
\end{whycode}
and we pass both files \texttt{maxsum\_\_MaxAndSum.ml} and
\texttt{main.ml} to the OCaml compiler:
\begin{verbatim}
> cd dir
> ocamlopt zarith.cmxa why3extract.cmxa maxsum__MaxAndSum.ml main.ml
\end{verbatim}
OCaml code extracted from \why must be linked with the library
\texttt{why3extract.cmxa} that is shipped with \why. It is typically
stored in subdirectory \texttt{why3} of the OCaml standard library.
Depending on the way \why was installed, it depends either on library
\texttt{nums.cmxa} or \texttt{zarith.cmxa} for big integers. Above we
assumed the latter. It is likely that additional options \texttt{-I}
must be passed to the OCaml compiler for libraries
\texttt{zarith.cmxa} and \texttt{why3extract.cmxa} to be found.
For instance, it could be
\begin{verbatim}
> ocamlopt -I `ocamlfind query zarith` zarith.cmxa \
           -I `why3 --print-libdir`/why3 why3extract.cmxa \
           ...
\end{verbatim}
To make the compilation process easier, one can write a
\texttt{Makefile} which can include informations about Why3
configuration as follows.
\begin{whycode}
WHY3SHARE=$(shell why3 --print-datadir)

include $(WHY3SHARE)/Makefile.config

maxsum:
        ocamlopt $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa \
                -o maxsum maxsum__MaxAndSum.ml main.ml
\end{whycode}



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