api.tex

\chapter{The \why API}
\label{chap:api}\index{API}
%HEVEA\cutname{api.html}

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\begin{latexonly}
at URL~\urlapi{}.\end{latexonly}
%HEVEA at this \ahref{\urlapi}{URL}.

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 in directory \verb|examples/use_api/| together
with a few other examples.

\lstset{language={[Objective]Caml}}

\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 $\mathit{true} \lor
\mathit{false}$.
\lstinputlisting{generated/logic__opening.ml}
The library uses the common type \texttt{term} both for terms
(\ie expressions that produce a value of some particular type)
and formulas (\ie 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.
\lstinputlisting{generated/logic__printformula.ml}

Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using
\begin{verbatim}
ocamlfind ocamlc -package why3 -linkpkg 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 us 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.
\lstinputlisting{generated/logic__declarepropvars.ml}
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.
\lstinputlisting{generated/logic__declarepropatoms.ml}

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 us 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 $\mathit{true} \lor
\mathit{false}$ above, this is done as follows.
\lstinputlisting{generated/logic__buildtask.ml}
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 that lemmas are not allowed in tasks
and can only be used in theories.

Once a task is built, it can be printed.
\lstinputlisting{generated/logic__printtask.ml}

The task for our second formula is a bit more complex to build, because
the variables A and B must be added as abstract (\ie not defined)
propositional symbols in the task.
\lstinputlisting{generated/logic__buildtask2.ml}

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}
\label{sec:api:callingprovers}

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.
\lstinputlisting{generated/logic__getconf.ml}
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
prover is a record with a name, a version, and an alternative description
(to differentiate between various configurations of a given prover). Its
definition is in the module \texttt{Whyconf}:
\lstinputlisting{generated/whyconf__provertype.ml}
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
attempt to access a prover named ``Alt-Ergo'', any version.
\lstinputlisting{generated/logic__getanyaltergo.ml}
We could also get a specific version with :
\lstinputlisting{generated/logic__getaltergo200.ml}

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.
\lstinputlisting{generated/logic__getdriver.ml}

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:
\lstinputlisting{generated/logic__callprover.ml}
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 an optional parameter \texttt{limit}, a record defined
in module \texttt{Call\_provers}:
\lstinputlisting{generated/call_provers__resourcelimit.ml}
where the field \texttt{limit\_time} is the maximum allowed running time in seconds,
and \texttt{limit\_mem} is the maximum allowed memory in megabytes.  The type
\texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:
\lstinputlisting{generated/call_provers__proverresult.ml}
with in particular the fields:
\begin{itemize}
\item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
\end{itemize}
A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:
\lstinputlisting{generated/call_provers__proveranswer.ml}
corresponding to these kinds 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 limit.
\item \texttt{OutOfMemory}: the prover exceeds the 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, \eg 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 (\eg 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.
\lstinputlisting{generated/logic__calltimelimit.ml}
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{sec:library}).
\lstinputlisting{generated/logic__buildfmla.ml}
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.
\lstinputlisting{generated/logic__buildtermalt.ml}

When building a task with this formula, we need to declare that we use
theory \texttt{Int}:
\lstinputlisting{generated/logic__buildtaskimport.ml}

\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}.
\lstinputlisting{generated/logic__quantfmla1.ml}
The next step is to introduce the variable $x$ with the type int.
\lstinputlisting{generated/logic__quantfmla2.ml}
The formula $x*x \geq 0$ is obtained as in the previous example.
\lstinputlisting{generated/logic__quantfmla3.ml}
To quantify on $x$, we use the appropriate smart constructor as follows.
\lstinputlisting{generated/logic__quantfmla4.ml}

\section{Building Theories}

We illustrate now how one can build theories. Building a theory must
be done by a sequence of calls:
\begin{itemize}
\item creating a theory ``under construction'', of type \verb|Theory.theory_uc|;
\item adding declarations, one at a time;
\item closing the theory under construction, obtaining something of type \verb|Theory.theory|.
\end{itemize}

Creation of a theory named \verb|My_theory| is done by
\lstinputlisting{generated/logic__buildth1.ml}
First let us add formula 1 above as a goal:
\lstinputlisting{generated/logic__buildth2.ml}
Note that we reused the goal identifier \verb|goal_id1| that we
already defined to create task 1 above.

Adding formula 2 needs to add the declarations of predicate variables A
and B first:
\lstinputlisting{generated/logic__buildth3.ml}

Adding formula 3 is a bit more complex since it uses integers, thus it
requires to ``use'' the theory \verb|int.Int|. Using a theory is
indeed not a primitive operation in the API: it must be done by a
combination of an ``export'' and the creation of a namespace. We
provide a helper function for that:
\lstinputlisting{generated/logic__buildth4.ml}
Addition of formula 3 is then
\lstinputlisting{generated/logic__buildth5.ml}

Addition of goal 4 is nothing more complex:
\lstinputlisting{generated/logic__buildth6.ml}

Finally, we close our theory under construction as follows.
\lstinputlisting{generated/logic__buildth7.ml}

We can inspect what we did by printing that theory:
\lstinputlisting{generated/logic__printtheory.ml}
which outputs
\begin{verbatim}
my new theory is as follows:

theory My_theory
  (* use BuiltIn *)

  goal goal1 : true \/ false

  predicate A

  predicate B

  goal goal2 : A /\ B -> A

  (* use int.Int *)

  goal goal3 : (2 + 2) = 4

  goal goal4 : forall x:int. (x * x) >= 0
end
\end{verbatim}

From a theory, one can compute at once all the proof tasks it contains
as follows:
\lstinputlisting{generated/logic__splittheory.ml}
Note that the tasks are returned in reverse order, so we reverse the
list above.

We can check our generated tasks by printing them:
\lstinputlisting{generated/logic__printalltasks.ml}

One can run provers on those tasks exactly as we did above.

\section{Operations on Terms and Formulas, Transformations}

The following code illustrates a simple recursive functions of
formulas. It explores the formula and when a negation is found, it
tries to push it down below a conjunction, a disjunction or a
quantifier.
\lstinputlisting{generated/transform__negate.ml}

The following illustrates how to turn such an OCaml function into a
transformation in the sense of the Why3 API. Moreover, it registers that
transformation to make it available for example in Why3 IDE.
\lstinputlisting{generated/transform__register.ml}

The directory \verb|src/transform| contains the code for the many
transformations that are already available in Why3.

\section{Proof Sessions}

See the example \verb|examples/use_api/create_session.ml| of the
distribution for an illustration on how to manipulate proof sessions
from an OCaml program.

\section{ML Programs}

The simplest way to build \whyml programs from OCaml is to build
untyped syntax trees for such programs, and then
call the \why typing procedure to build typed declarations.

The examples of this section are available in the file
\verb|examples/use_api/mlw_tree.ml| of the distribution.

The first step is to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}, and open the OCaml module
\verb|Ptree| which contains most of the OCaml functions we need in
this section.
\lstinputlisting{generated/mlw_tree__buildenv.ml}

To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following
declarations, that first introduces a pseudo ``file'' to hold the
module, then the module itself called \verb|Program|.
\lstinputlisting{generated/mlw_tree__openmodule.ml}
Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without
any attributes nor any location.

To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally
imports \verb|int.Int|.
\lstinputlisting{generated/mlw_tree__useimport.ml}

We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}

The OCaml code that programmatically build this Why3 function is as follows.
\lstinputlisting{generated/mlw_tree__code1.ml}
This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}.
\begin{figure}[t]
  \lstinputlisting{generated/mlw_tree__helper1.ml}
  \caption{Helper functions for building WhyML programs}
  \label{fig:helpers}
\end{figure}

We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
\lstinputlisting{generated/mlw_tree__code2.ml}

The next example makes use of arrays.
\lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}
The corresponding OCaml code is as follows
\lstinputlisting{generated/mlw_tree__code3.ml}

Having declared all the programs we wanted to write, we can now close
the module and the file, and get as a result the set of modules of our
file, under the form of a map of module names to modules.
\lstinputlisting{generated/mlw_tree__closemodule.ml}

We can then construct the proofs tasks for our module, and then try to
call the Alt-Ergo prover. The rest of that code is using OCaml
functions that were already introduced before.
\lstinputlisting{generated/mlw_tree__checkingvcs.ml}

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