Commit ef2899d2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve documentation a bit.

parent b484b2b1
......@@ -360,13 +360,13 @@ be done by a sequence of calls:
\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:
Creation of a theory named \verb|My_theory| is done by
\begin{ocamlcode}
let my_theory : Theory.theory_uc =
Theory.create_theory (Ident.id_fresh "My_theory")
\end{ocamlcode}
First let us add the formula 1 above as a goal:
First let us add formula 1 above as a goal:
\begin{ocamlcode}
let decl_goal1 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
......@@ -424,7 +424,7 @@ Finally, we close our theory under construction as follows.
let my_theory : Theory.theory = Theory.close_theory my_theory
\end{ocamlcode}
We can inspect what we did for example by printing that theory:
We can inspect what we did by printing that theory:
\begin{ocamlcode}
let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
\end{ocamlcode}
......@@ -472,21 +472,21 @@ let () =
One can run provers on those tasks exactly as we did above.
\section{Applying transformations}
\section{Applying Transformations}
[TO BE COMPLETED]
\section{Writing new functions on term}
\section{Writing New Functions on Terms}
[TO BE COMPLETED]
% pattern-matching on terms, opening a quantifier
\section{Proof sessions}
\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}
\section{ML Programs}
There are two ways for building \whyml programs from OCaml. The first
is to build untyped syntax trees for such \whyml programs, and then
......
......@@ -14,7 +14,7 @@ The Coq tactic is installed in
where \textit{why3-lib-dir} is \why's library directory, as reported
by \verb+why3 --print-libdir+. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3ide}, \texttt{why3replay},
calling Coq via \why (from \texttt{why3 ide}, \texttt{why3 replay},
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path, either using Coq's command line
option \texttt{-I} or by adding
......@@ -33,6 +33,7 @@ The Coq tactic is called \texttt{why3} and is used as follows:
The string \textit{prover-name} identifies one of the automated theorem provers
supported by \why, as reported by \verb+why3 --list-provers+
(interactive provers excluded).
\index{list-provers@\verb+--list-provers+}
The current goal is then translated to \why's logic and the prover is
called. If it reports the goal to be valid, then Coq's \texttt{admit}
tactic is used to assume the goal. The prover is called with a time
......
......@@ -34,7 +34,8 @@ It is also installable from sources, downloadable from the site
\noindent
For some of the \why tools, additional OCaml libraries are needed:
\begin{itemize}
\item For the graphical interface: the Lablgtk2 library for OCaml
\item For the graphical interface, the Lablgtk2 library is needed.
It provides OCaml
bindings of the gtk2 graphical library. For Debian-based Linux
distributions, you can install the packages
\begin{verbatim}
......@@ -43,7 +44,8 @@ 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{why3 bench}: The OCaml bindings of the sqlite3 library.
\item For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library
are needed.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
......@@ -91,7 +93,7 @@ Everything OK.
\end{verbatim}
\end{enumerate}
\section{Local use, without installation}
\section{Local Use, Without Installation}
It is not mandatory to install \why into system directories.
\why can be configured and compiled for local use as follows:
......@@ -127,7 +129,7 @@ Section~\ref{sec:why3config}.
\section{Multiple Versions of the Same Prover}
Since version 0.72, \why is able to use several versions of the same
\why is able to use several versions of the same
prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
The automatic detection of provers looks for typical names for their
executable command, \eg \texttt{cvc3} for CVC3. However, if you
......@@ -136,6 +138,7 @@ 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| with the
\texttt{config} command, \eg
\index{add-prover@\verb+--add-prover+}
\begin{verbatim}
why3 config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
\end{verbatim}
......
......@@ -87,7 +87,7 @@ tracking system.)
The result of provers detection is stored in the user's
configuration file (\verb+~/.why3.conf+ or, in the case of local
installation, \verb+why3.conf+ in Why3 sources top directory). This file
installation, \verb+why3.conf+ in \why sources top directory). This file
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg different
versions of the same prover, or with different options.
......@@ -143,15 +143,16 @@ The \texttt{prove} command executes the following steps:
\item Parse and typecheck the given files using the correct parser in order
to obtain a set of \why theories for each file. It uses
the filename extension or the \verb|--format| option to choose
among the available parsers. The \verb|--list-format| option gives
the list of registered parsers.
among the available parsers. \verb|why3 --list-formats| lists
the registered parsers.
\index{list-formats@\verb+--list-formats+}
\whyml modules are turned into
theories containing verification conditions as goals.
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using options
\verb|-G/--goal| and \verb|-T/--theory|. Option
\verb|-T/--theory| applies to the last file appearing on the
command line, the option \verb|-G/--goal| applies to the last theory
\verb|-T/--theory| applies to the previous file appearing on the
command line. Option \verb|-G/--goal| applies to the previous theory
appearing on the command line. If no theories are selected in a file,
then every theory is considered as selected. If no goals are selected
in a theory, then every goal is considered as selected.
......@@ -159,21 +160,22 @@ The \texttt{prove} command executes the following steps:
\index{goal@\verb+--goal+}
\index{T@\verb+-T+|see{\texttt{-{}-theory}}}
\index{theory@\verb+--theory+}
\item Apply the transformation requested
\item Apply the transformations requested
with \verb|-a/--apply-transform| in their order of appearance on the
command line. \verb|--list-transforms| lists the known
transformations, plugins can add more of them.
command line. \verb|why3 --list-transforms| lists the known
transformations; plugins can add more of them.
\index{a@\verb+-a+|see{\texttt{-{}-apply-transform}}}
\index{apply-transform@\verb+--apply-transform+}
\index{list-transforms@\verb+--list-transforms+}
\item Apply the driver selected with the \verb|-D/--driver| option,
or the driver of the prover selected with the \verb|-P/--prover|
option. \verb|--list-provers| lists the known provers, \ie the ones
option. \verb|why3 --list-provers| lists the known provers, \ie the ones
that appear in the configuration file.
\index{D@\verb+-D+|see{\texttt{-{}-driver}}}
\index{driver@\verb+--driver+}
\index{P@\verb+-P+|see{\texttt{-{}-prover}}}
\index{prover@\verb+--prover+}
\index{list-provers@\verb+--list-provers+}
\item If option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If option
\verb|-D/--driver| is given, print each generated task using
......@@ -509,7 +511,6 @@ of the definitions is irrelevant. Notice that one can use
axiomatizations.
One can run all the bench given in one bench configuration file with
\texttt{why3bench}:
\begin{verbatim}
why3 bench -B path_to_my_bench.rc
\end{verbatim}
......@@ -989,7 +990,7 @@ add the option \verb|-F| to force this behavior.
\section{The \texttt{doc} command}
\section{The \texttt{doc} Command}
\label{sec:why3doc}
This tool can produce HTML pages from \why source code.
......
......@@ -250,6 +250,7 @@ Known provers:
coq (Coq)
simplify (Simplify)
\end{verbatim}
\index{list-provers@\verb+--list-provers+}
The first word of each line is a unique identifier for the associated prover. We thus
have now the three provers Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
......
......@@ -11,7 +11,7 @@ These declarations can be directly written in the theory or taken from
existing theories. The base logic of \why is first-order
logic with polymorphic types.
\section{Example 1: lists}
\section{Example 1: Lists}
%BEGIN LATEX
Figure~\ref{fig:tutorial1} contains an example of \why input
......@@ -56,7 +56,8 @@ theory Sorted
end
\end{whycode}
%BEGIN LATEX
\caption{Example of Why3 text.}
\vspace*{-1em}%\hrulefill
\caption{Example of \why text}
\label{fig:tutorial1}
\end{figure}
%END LATEX
......@@ -118,7 +119,7 @@ Note that the type signature of \lstinline{sorted} predicate does not
include the name of a parameter (see \texttt{l} in the definition
of \texttt{length}): it is unused and therefore optional.
\section{Example 1 (continued): lists and abstract orderings}
\section{Example 1 (continued): Lists and Abstract Orderings}
In the previous section we have seen how a theory can reuse the
declarations of another theory, coming either from the same input
......@@ -171,7 +172,8 @@ theory SortedIntList
end
\end{whycode}
%BEGIN LATEX
\caption{Example of Why3 text (continued).}
\vspace*{-1em}%\hrulefill
\caption{Example of \why text (continued)}
\label{fig:tutorial2}
\end{figure}
%END LATEX
......@@ -307,10 +309,10 @@ namespace import O
clone export Order
end
\end{whycode}
However, since \why favours short theories over long and complex ones,
However, since \why favors short theories over long and complex ones,
this feature is rarely used.
\section{Example 2: Einstein's problem}
\section{Example 2: Einstein's Problem}
\index{Einstein's logic problem}
We now consider another, slightly more complex example: how to use \why
......@@ -323,7 +325,7 @@ problem''.%
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
These five persones own different pets, drink different beverages and
These five persons own different pets, drink different beverages and
smoke different brands of cigars.
We are given the following information:
\begin{itemize}
......
......@@ -10,7 +10,7 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu
\lstinputlisting{../share/why3session.dtd}
\section{Provers detection data}
\section{Prover Detection}
\label{sec:proverdetecttiondata}
All the necessary data configuration for the automatic detection of
......@@ -26,12 +26,31 @@ file is reproduced below.
}
%END LATEX
\section{The \texttt{why3.conf} configuration file}
\section{The \texttt{why3.conf} Configuration File}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
\begin{figure}[p]
One can use a custom configuration file. The \why
tools look for it in the following order:
\begin{enumerate}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set,
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in the top directory of \why sources.
\end{enumerate}
If none of these files exist, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections.
%BEGIN LATEX
Figure~\ref{fig:why3conf} shows an example of configuration file.
%END LATEX
%HEVEA Below is an example of configuration file.
%BEGIN LATEX
\begin{figure}[p]
{\footnotesize
%END LATEX
\begin{verbatim}
......@@ -90,28 +109,10 @@ name = "CoqIDE"
\end{verbatim}
%BEGIN LATEX
}
%END LATEX
\caption{Sample why3.conf file}
\caption{Sample \texttt{why3.conf} file}
\label{fig:why3conf}
\end{figure}
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools look for it in the following order:
\begin{enumerate}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set,
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in the top directory of \why sources.
\end{enumerate}
If none of these files exists, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Figure~\ref{fig:why3conf}
shows an example of configuration file.
%END LATEX
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
......@@ -121,15 +122,16 @@ argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.
Sections contain associations \texttt{key=value}. A value is either
an integer (\eg{} -555), a boolean (true, false), or a string (\eg
"emacs"). Some specific keys can be attributed multiple values and are
an integer (\eg \texttt{-555}), a boolean (\texttt{true}, \texttt{false}),
or a string (\eg \texttt{"emacs"}). Some specific keys can be attributed
multiple values and are
thus allowed to occur several times inside a given section. In that
case, the relative order of these associations matter.
\section{Drivers of External Provers}
\section{Drivers for External Provers}
\label{sec:drivers}
Drivers of external provers are readable files from directory
Drivers for external provers are readable files from directory
\texttt{drivers}. Experimented users can modify them to change the way
the external provers are called, in particular which transformations
are applied to goals.
......@@ -148,6 +150,7 @@ installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
\index{list-transforms@\verb+--list-transforms+}
\subsection{Non-splitting transformations}
......@@ -220,7 +223,6 @@ definitions~\cite{paskevich09rr}.
\item[inline\_trivial]
removes definitions of the form
\begin{whycode}
function f x_1 ... x_n = (g e_1 ... e_k)
predicate p x_1 ... x_n = (q e_1 ... e_k)
......
......@@ -129,7 +129,7 @@ pattern matching immediately:
We are now left with the function body itself, that is a code
computing the sum and the maximum of all elements in \texttt{a}. With
no surpise, it is as simple as introducing two local references
no surprise, it is as simple as introducing two local references
\begin{whycode}
let sum = ref 0 in
let max = ref 0 in
......@@ -192,7 +192,7 @@ end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 1.}
\caption{Solution for VSTTE'10 competition problem 1}
\label{fig:MaxAndSum}
\end{figure}
%END LATEX
......@@ -315,7 +315,7 @@ end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
\caption{Solution for VSTTE'10 competition problem 2}
\label{fig:Inverting}
\end{figure}
%END LATEX
......@@ -441,7 +441,7 @@ end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 3.}
\caption{Solution for VSTTE'10 competition problem 3}
\label{fig:LinkedList}
\end{figure}
%END LATEX
......@@ -613,7 +613,7 @@ module NQueens
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (1/2).}
\caption{Solution for VSTTE'10 competition problem 4 (1/2)}
\label{fig:NQueens1}
\end{figure}
%END LATEX
......@@ -766,7 +766,7 @@ end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (2/2).}
\caption{Solution for VSTTE'10 competition problem 4 (2/2)}
\label{fig:NQueens2}
\end{figure}
%END LATEX
......@@ -947,7 +947,7 @@ end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 5.}
\caption{Solution for VSTTE'10 competition problem 5}
\label{fig:AQueue}
\end{figure}
%END LATEX
......
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