Commit 0285a2ab authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update documentation.

parent 97750ea5
......@@ -17,7 +17,7 @@ the maximum and the sum of an array of integers.
Let us assume it is contained in a file \texttt{maxsum.mlw}.
\section{Interpreting \whyml Code}
\index{exec@\verb+--exec+}\index{interpretation!of \whyml}
\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
......@@ -30,29 +30,28 @@ in module \texttt{MaxAndSum}
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 option \verb+--exec+ to interpret this function,
and then we use the \texttt{execute} command to interpret this function,
as follows:
\begin{verbatim}
> why3 maxsum.mlw --exec MaxAndSum.test
Execution of MaxAndSum.test ():
type: (int, int)
result: Tuple2(45, 10)
globals:
> why3 execute maxsum.mlw MaxAndSum.test
Execution of MaxAndSum.test ():
type: (int, int)
result: Tuple2(45, 10)
globals:
\end{verbatim}
We get the expected output, namely the pair \texttt{(45, 10)}.
\section{Compiling \whyml to OCaml}
\index{OCaml}\index{extraction}
\index{E@\verb+-E+|see{\texttt{-{}-extract}}}
\index{extract@\verb+--extract+}
\index{extract@\texttt{extract}}
An alternative to interpretation is to compile \whyml to OCaml.
We do so using option \verb+--extract+, as follows:
We do so using the \texttt{extract} command, as follows:
\begin{verbatim}
> mkdir dir
> why3 --extract ocaml64 maxsum.mlw -o dir
> mkdir dir
> why3 extract -D ocaml64 maxsum.mlw -o dir
\end{verbatim}
Option \verb+--extract+ requires the name of a driver, which indicates
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
......@@ -74,8 +73,8 @@ containing a call to \texttt{test}, that is, for example,
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
> 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
......@@ -87,9 +86,9 @@ 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 \
...
> ocamlopt -I `ocamlfind query zarith` zarith.cmxa \
-I `why3 --print-libdir`/why3 why3extract.cmxa \
...
\end{verbatim}
......
......@@ -43,7 +43,7 @@ liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item For \texttt{why3bench}: The OCaml bindings of the sqlite3 library.
\item For \texttt{why3 bench}: The OCaml bindings of the sqlite3 library.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
......@@ -70,10 +70,10 @@ Installation is performed (as super-user if needed) using
\begin{verbatim}
make install
\end{verbatim}
Installation can be tested as follows:
Installation can be tested as follows:
\begin{enumerate}
\item install some external provers (see~Section~\ref{provers} below)
\item run \verb|why3config --detect|
\item run \verb|why3 config --detect|
\item run some examples from the distribution, \eg you should
obtain the following:
\begin{verbatim}
......@@ -136,10 +136,10 @@ executable command, \eg \texttt{cvc3} for CVC3. However, if you
install several version of the same prover it is likely that you would
use specialized executable names, such as \texttt{cvc3-2.2} or
\texttt{cvc3-2.4.1}. To allow the \why detection process to recognize
these, you can use the option \verb|--add-prover| to
\texttt{why3config}, \eg
these, you can use the option \verb|--add-prover| with the
\texttt{config} command, \eg
\begin{verbatim}
why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
why3 config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
\end{verbatim}
the first argument (here \verb|cvc3-2.4|) must be one of the class of
provers known in the file \verb|provers-detection-data.conf| typically
......@@ -177,12 +177,12 @@ each prover, in the \why configuration file. Within the GUI, you can
discard these choices via the \textsf{Preferences} dialog.
Outside the GUI, the prover upgrades are handled as follows. The
\texttt{why3replayer} tool will just ignore proof attempts marked as
\texttt{replayer} command will just ignore proof attempts marked as
archived\index{archived}.
Conversely, a non-archived proof attempt with a non-existent
prover will be reported as a replay failure. The tool
\texttt{why3session} allows you to perform move or copy operations on
proof attempts in a fine-grain way, using filters, as detailed in
prover will be reported as a replay failure. The
\texttt{session} command performs move or copy operations on
proof attempts in a fine-grained way, using filters, as detailed in
Section~\ref{sec:why3session}.
......
......@@ -36,18 +36,22 @@ assistant) to ease some proofs.
\subsection{Generating a realization}
Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
Generating the skeleton for a theory is done by passing to the
\texttt{realize} command a driver suitable for realizations, the names of
the theories to realize, and a target directory.
\index{realize@\verb+--realize+}
\index{realize@\texttt{realize}}
\begin{verbatim}
why3 --realize -D path/to/drivers/prover-realize.drv
-T env_path.theory_name -o path/to/target/dir/
why3 realize -D path/to/drivers/prover-realize.drv
-T env_path.theory_name -o path/to/target/dir/
\end{verbatim}
\index{driver@\verb+--driver+}
\index{theory@\verb+--theory+}
The theory is looked into the files from the environment, \eg the standard
library. If the theory is stored in a different location, option \texttt{-L}
should be used.
The name of the generated file is inferred from the theory name. If the
target directory already contains a file with the same name, \why
extracts all the parts that it assumes to be user-edited and merges them in
......
This diff is collapsed.
......@@ -42,7 +42,7 @@ refer to Section~\ref{sec:ideref} for a more complete description.
The GUI is launched on the file above as follows.
\begin{verbatim}
why3ide hello_proof.why
why3 ide hello_proof.why
\end{verbatim}
When the GUI is started for the first time, you should get a window
that looks like the screenshot of Figure~\ref{fig:gui1}.
......@@ -190,12 +190,12 @@ you must select the context \textsf{all goals} at the top of the left
tool bar.
Notice that replaying can be done in batch mode, using the
\texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For
\texttt{replayer} command (see Section~\ref{sec:why3replayer}) For
example, running the replayer on the \texttt{hello\_proof} example is
as follows (assuming $G_2$ still is
\lstinline|(true -> false) /\ (true \/ false)|).
\begin{verbatim}
$ why3replayer hello_proof
$ why3 replayer hello_proof
Info: found directory 'hello_proof' for the project
Opening session...[Xml warning] prolog ignored
[Reload] file '../hello_proof.why'
......@@ -229,7 +229,7 @@ attempt for the same goal.
\section{Getting Started with the \why Command}
\label{sec:batch}
The why3 command allows to check the validity of goals with external
The \texttt{prove} command allows to check the validity of goals with external
provers, in batch mode. This section presents the basic use of this
tool. Refer to Section~\ref{sec:why3ref} for a more complete
description of this tool and all its command-line options.
......@@ -239,7 +239,7 @@ autodetection of external provers. We have already seen how to do
it in the \why GUI. On the command line, this is done as follows
(here ``\texttt{>}'' is the prompt):
\begin{verbatim}
> why3config --detect
> why3 config --detect
\end{verbatim}
This prints some information messages on what detections are attempted. To know which
provers have been successfully detected, you can do as follows.
......@@ -254,24 +254,24 @@ The first word of each line is a unique identifier for the associated prover. We
have now the three provers Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
Let's assume now we want to run Simplify on the HelloProof
Let us assume that we want to run Simplify on the HelloProof
example. The command to type and its output are as follows, where the
\verb|-P| option is followed by the unique prover identifier (as shown
by \texttt{--list-provers} option).
\begin{verbatim}
> why3 -P simplify hello_proof.why
> why3 prove -P simplify hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.10s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
\end{verbatim}
Unlike \why GUI, the command-line tool does not save the proof attempts
Unlike the \why GUI, the command-line tool does not save the proof attempts
or applied transformations in a database.
We can also specify which goal or goals to prove. This is done by giving
first a theory identifier, then goal identifier(s). Here is the way to
call Alt-Ergo on goals $G_2$ and $G_3$.
\begin{verbatim}
> why3 -P alt-ergo hello_proof.why -T HelloProof -G G2 -G G3
> why3 prove -P alt-ergo hello_proof.why -T HelloProof -G G2 -G G3
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Valid (0.01s)
\end{verbatim}
......@@ -292,7 +292,7 @@ Known splitting transformations:
Here is how you can split the goal $G_2$ before calling
Simplify on resulting subgoals.
\begin{verbatim}
> why3 -P simplify hello_proof.why -a split_goal -T HelloProof -G G2
> why3 prove -P simplify hello_proof.why -a split_goal -T HelloProof -G G2
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G2 : Valid (0.00s)
\end{verbatim}
......
......@@ -38,12 +38,12 @@ They also provide extra features:
Programs are contained in files with suffix \verb|.mlw|.
They are handled by \texttt{why3}. For instance
\begin{verbatim}
> why3 myfile.mlw
> why3 prove myfile.mlw
\end{verbatim}
will display the verification conditions extracted from modules in
file \texttt{myfile.mlw}, as a set of corresponding theories, and
\begin{verbatim}
> why3 -P alt-ergo myfile.mlw
> why3 prove -P alt-ergo myfile.mlw
\end{verbatim}
will run the SMT solver Alt-Ergo on these verification conditions.
Program files are also handled by the GUI tool \texttt{why3ide}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment