Commit 7fe22482 authored by MARCHE Claude's avatar MARCHE Claude

more in roadmap

small modifs in the manual
parent d6d59f63
......@@ -53,6 +53,8 @@
* complete doc/api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* rename andb, orb, xorb and notb into and, or, xor and not
=== Roadmap for third release 0.70 =======================================
* Final preparation: put on the web page
......@@ -61,6 +63,8 @@
** API doc in HTML (suggestion: http://why3.lri.fr/api/)
Note: check that URL of API doc is correct in doc/api.tex line 9.
* doc: citer l'article Boogie 2011 quelque part
* Check if remark in doc/api.tex line 80 is still valid (A)
* increment the magic number in config (A)
......
\chapter{The \why\ API}
\chapter{The \why API}
\label{chap:api}
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
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
at URL~\url{http://why3.lri.fr/api/}.
We assume the reader has a fair knowledge of the OCaml
language. Notice that the \why\ library must be installed, see
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 as \url{examples/use_api.ml}.
......@@ -80,7 +80,7 @@ As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A /\ B -> A
\end{verbatim}
\todo{Check: Notice that the concrete syntax of \why\ forbids predicate identifiers
\todo{Check: Notice that the concrete syntax of \why forbids predicate identifiers
to start with a capital letter. This constraint does not exist when
building those directly using library calls.}
......@@ -102,7 +102,7 @@ let task1 : Task.task =
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
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}
......
\chapter{Tools}
\label{chap:tools}
\section{\why\ command line tool}
\section{\why command line tool}
\section{IDE}
......
......@@ -3,7 +3,7 @@
\section{Architecture and Terminology}
Everything in \why\ revolves around the notion of
Everything in \why revolves around the notion of
\emph{task}\index{task}. \why, as a platform, is a tool that
translates its input to a number of tasks, and dispatches these tasks
to external provers.
......@@ -32,7 +32,7 @@ manuals, giving detailed technical informations.
Chapter~\ref{chap:starting} explains how to get started with the Why
IDE for visualizing theories and goals, calling external provers for
trying to solve them, and applying transformations to simplify
them. It also presents the basic use of \why\ in
them. It also presents the basic use of \why in
batch. Chapter~\ref{chap:syntax} presents the input syntax for file
defining Why theories. The semantics is given informally with
examples. The two first chapters are thus to read for the beginners.
......@@ -43,9 +43,9 @@ examples. The two first chapters are thus to read for the beginners.
% next chapters are for users with a little more experience, in
% particular those who wants to use Why for verification of algorithms.
Chapter~\ref{chap:api} presents how to use \why\ programmatically,
Chapter~\ref{chap:api} presents how to use \why programmatically,
using the API. It is for the experimented users, who wants to link
\why\ library with their own code.
\why library with their own code.
Part 2 provides:
\begin{itemize}
......
\newcommand{\todo}[1]{{\Huge\bfseries #1}}
\newcommand{\why}{\textsf{Why3}}
\newcommand{\whyml}{\textsf{Why3ML}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
\newcommand{\eg}{\emph{e.g.}}
% BNF grammar
......
\chapter{Reference manuals for the \why\ tools}
\chapter{Reference manuals for the \why tools}
\label{chap:manpages}
\section{Compilation, Installation}
\label{sec:install}
Compilation of \why\ must start with a configuration phase which is run as
Compilation of \why must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
......@@ -21,17 +21,18 @@ It is also installable from sources, downloadable from the site
\url{http://caml.inria.fr/ocaml/}
\end{itemize}
For the IDE, additional OCaml libraries are needed:
For some tools, additional OCaml libraries are needed:
\begin{itemize}
\item The Lablgtk2 library for OCaml bindings of the gtk2 graphical library.
For Debian-based Linux distributions, you can install the packages
\item For the IDE: the Lablgtk2 library for OCaml bindings of the gtk2
graphical library. For Debian-based Linux distributions, you can
install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item The OCaml bindings of the sqlite3 library.
\item For \texttt{why3bench}: The OCaml bindings of the sqlite3 library.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
......@@ -47,18 +48,18 @@ make
\subsection{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:
It is not mandatory to install \why into system directories.
\why can be configured and compiled for local use as follows:
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
The \why\ executables are then available in the subdirectory \texttt{bin/}.
The \why executables are then available in the subdirectory \texttt{bin/}.
\subsection{Installation of the \why\ library}
\subsection{Installation of the \why library}
\label{sec:installlib}
By default, the \why\ library is not installed. It can be installed using
By default, the \why library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
......@@ -66,21 +67,21 @@ make install_lib
\section{Installation of external provers}
\why\ can use a wide range of external theorem provers. These need to
be installed separately, and then \why\ needs to be configured to use
\why can use a wide range of external theorem provers. These need to
be installed separately, and then \why needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why.
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
For configuring \why\ to use the provers, follow instructions given in
For configuring \why to use the provers, follow instructions given in
Section~\ref{sec:why3config}.
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
\why\ must be configured to access external provers. Typically, this is done
\why must be configured to access external provers. Typically, this is done
by running either the command line tool
\begin{verbatim}
why3config
......@@ -91,9 +92,9 @@ File/Detect provers
\end{verbatim}
of the IDE. This must be redone each time a new prover is installed.
The provers which \why\ attempts to detect are described in
The provers which \why attempts to detect are described in
the readable configuration file \texttt{provers-detection-data.conf}
of the \why\ data directory (\eg{}
of the \why data directory (\eg{}
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
......@@ -114,13 +115,14 @@ The provers which are typically looked for are
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
\item Spass~: \url{http://www.spass-prover.org/}
\item veriT~: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}
\item Spass: \url{http://www.spass-prover.org/}
\item Vampire: \url{http://www.voronkov.com/vampire.cgi}
\item VeriT: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}, only versions 1.xx since versions 2.xx do not support quantifiers
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
\end{itemize}
\texttt{why3config} also detects the plugins installed in the \why\
\texttt{why3config} also detects the plugins installed in the \why
plugins directory (\eg{} \texttt{/usr/local/lib/why3/plugins}). A
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.
......@@ -129,15 +131,15 @@ If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value,
but will not try to detect provers.
The option \texttt{--detect-provers} should be used to force
\why\ to detect again the available
\why to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--detect-plugins} will do the same for plugins.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
\why\ is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why\ language
\why is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.
......@@ -150,7 +152,7 @@ The \texttt{why3} tool executes the following steps:
\item Load the plugins mentioned in the configuration. It will not
stop if some plugin fails to load.
\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
to obtain a set of \why theories for each file. It uses
the filename extension or the \texttt{--format} option to choose
among the available parsers. The \texttt{--list-format} option gives
the list of registered parsers.
......@@ -187,7 +189,7 @@ The provers can answer the following output:
\item[Failure] an error occured,
\item[Invalid] the prover know the goal can't be proved
\end{description}
% \why\ can also be *)
% \why can also be *)
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
......@@ -295,11 +297,11 @@ The preferences window allows you customize
\section{The \texttt{why3ml} tool}
\texttt{why3ml} is an additional layer on \why\ library for
generating verification conditions from \whyml\ programs.
\texttt{why3ml} is an additional layer on \why library for
generating verification conditions from \whyml programs.
The command-line of \texttt{why3ml} is identical to that of
\texttt{why3}, but also accepts files with extension \texttt{.mlw} as
input files containing \whyml\ modules (see chapter~\ref{chap:whyml}
input files containing \whyml modules (see chapter~\ref{chap:whyml}
and section~\ref{sec:syntax:whyml}). Modules are turned into
theories containing verification conditions as goals, and then
\texttt{why3ml} behaves exactly as \texttt{why3} for the remaining of
......@@ -312,7 +314,7 @@ For those who want to experiment with \whyml, many examples are provided in
\section{The \texttt{why3bench} tool}
The \texttt{why3bench} tool adds a scheduler on top of the \why\
The \texttt{why3bench} tool adds a scheduler on top of the \why
library. \texttt{why3bench} is designed to compare various components
of automatic proofs: automatic provers, transformations, definitions
of a theory. For that goal it tries to prove predefined goals using
......
......@@ -6,6 +6,7 @@
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
\usepackage{graphicx}
\usepackage{xspace}
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
......@@ -92,25 +93,24 @@ $^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\chapter*{Foreword}
This is the manual for the Why platform version 3, or \why\ for
short. \why\ is a complete reimplementation of the former Why
This is the manual for the Why platform version 3, or \why for
short. \why is a complete reimplementation of the former Why
platform~\cite{filliatre07cav} for program verification. Among
the new features are: numerous extensions to the input language,
a new architecture for calling external provers, and a
well-designed API, allowing to use \why\ as a software library.
well-designed API, allowing to use \why as a software library.
An important emphasis is put on modularity and genericity,
giving the end user a possibility to easily reuse \why\
giving the end user a possibility to easily reuse \why
formalizations or to add support for a new external
prover if wanted.
\subsection*{Availability}
\why\ project page is \url{http://why3.gforge.inria.fr/}.
%\url{https://gforge.inria.fr/projects/why3}.
The last distribution is available, in source format, together with
this documentation and several examples.
\why project page is \url{http://why3.lri.fr/}. The last
distribution is available, in source format, together with this
documentation and several examples.
\why\ is distributed as open source and freely available under the
\why is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.
See the file \texttt{INSTALL} for quick installation instructions, and
......@@ -122,7 +122,7 @@ instructions.
There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.
Report any bug to the \why\ Bug Tracking System:
Report any bug to the \why Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.
......
......@@ -3,12 +3,12 @@
\section{Hello Proofs}
The first and basic step in using \why\ is to write a suitable input
The first and basic step in using \why is to write a suitable input
file. When one wants to learn a programming language, you start by
writing a basic program. Here we start by writing a file containing a
basic set of goals.
Here is our first \why\ file, which is the file
Here is our first \why file, which is the file
\texttt{examples/hello\_proof.why} of the distribution.
\verbatiminput{../examples/hello_proof.why}
......@@ -17,12 +17,12 @@ inside a theory, which is in that example called TheoryProof and
labelled with a comment inside double quotes. It contains three goals
named $G_1,G_2,G_3$. The first two are basic propositional goals,
whereas the third involves some integer arithmetic, and thus it
requires to import the theory of integer arithmetic from the \why\
requires to import the theory of integer arithmetic from the \why
standard library, which is done by the \texttt{use} declaration above.
We don't give more details here about the syntax and refer to
Chapter~\ref{chap:syntax} for detailed explanations. In the following,
we show how this file is handled in the \why\ GUI
we show how this file is handled in the \why GUI
(Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
executable (Section~\ref{sec:batch}).
......@@ -160,7 +160,7 @@ Starting the IDE on the modified file and expanding everything with
The important feature to notice first is that all the previous proof
attempts and transformations were saved in a database --- an SQLite3
file created when the \why\ file was opened in the GUI for the first
file created when the \why file was opened in the GUI for the first
time. Then, for
all the goals that remain unchanged, the previous proofs are shown
again. For the parts that changed, the previous proofs attempts are
......@@ -168,7 +168,7 @@ shown but marked with "(obsolete)" so that you know the results are
not accurate. You can now retry to prove all what remains unproved
using any of the provers, using the button ``Replay''.
\section{Getting Started with the \why\ Command}
\section{Getting Started with the \why Command}
\label{sec:batch}
The why3 command allows to check the validity of goals with external
......@@ -178,7 +178,7 @@ description of this tool and all its command-line options.
The very first time you want to use Why, you should proceed with
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
it in the \why GUI. On the command line, this is done as follows
(here ``\texttt{>}'' is the prompt):
\begin{verbatim}
> why3config --detect
......
\chapter{The \why\ Language}
\chapter{The \why Language}
\label{chap:syntax}
This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples.
A \why\ text contains a list of \emph{theories}.
A \why text contains a list of \emph{theories}.
A theory is a list of \emph{declarations}. Declarations introduce new
types, functions and predicates, state axioms, lemmas and goals.
These declarations can be directly written in the theory or taken from
existing theories. The base logic of \why\ is first-order
existing theories. The base logic of \why is first-order
logic with polymorphic types.
\subsection{Example 1: lists}
The Figure~\ref{fig:tutorial1} contains an example of \why\ input
The Figure~\ref{fig:tutorial1} contains an example of \why input
text, containing three theories. The first theory, \texttt{List},
declares a new algebraic type for polymorphic lists, \texttt{list 'a}.
As in ML, \texttt{'a} stands for a type variable.
......@@ -80,13 +80,13 @@ The next declaration defines a recursive function, \texttt{length},
which computes the length of a list. The \texttt{function} and
\texttt{predicate} keywords are used to introduce function and
predicate symbols, respectively.
\why\ checks every recursive, or mutually recursive, definition for
\why checks every recursive, or mutually recursive, definition for
termination. Basically, we require a lexicographic and structural
descent for every recursive call for some reordering of arguments.
Notice that matching must be exhaustive and that every \texttt{match}
expression must be terminated by the \texttt{end} keyword.
Despite using higher-order ``curried'' syntax, \why\ does not permit
Despite using higher-order ``curried'' syntax, \why does not permit
partial application: function and predicate arities must be respected.
The last declaration in theory \texttt{Length} is a lemma stating that
......@@ -172,7 +172,7 @@ Consider theory \texttt{SortedGen}. In the beginning, we
make a simple \texttt{clone} theory \texttt{Order}.
This is pretty much equivalent to copy-pasting every
declaration from \texttt{Order} to \texttt{SortedGen};
the only difference is that \why\ traces the history
the only difference is that \why traces the history
of cloning and transformations and drivers often make
use of it (see Section~\ref{sec:drivers}).
......@@ -198,7 +198,7 @@ ordered type, without having to retype the definition of
makes \texttt{clone} of \texttt{SortedGen} (\emph{i.e.}~copies its
declarations) substituting type \texttt{int} for type
\texttt{O.t} of \texttt{SortedGen} and the default order
on integers for predicate \texttt{O.(<=)}. \why\ will
on integers for predicate \texttt{O.(<=)}. \why will
control that the result of cloning is well-typed.
Several remarks ought to be made here. First of all, why should
......@@ -215,8 +215,8 @@ is not copied from the theory being cloned. Thus, we will not create
a second declaration of type \texttt{int} in \texttt{SortedIntList}.
The mechanism of cloning bears some resemblance to modules and functors
of ML-like languages. Unlike those languages, \why\ makes no distinction
between modules and module signatures, modules and functors. Any \why\
of ML-like languages. Unlike those languages, \why makes no distinction
between modules and module signatures, modules and functors. Any \why
theory can be \texttt{use}'d directly or instantiated in any of its
abstract symbols.
......@@ -283,7 +283,7 @@ is later used under the name \texttt{T}, the name of the symbol
would be \texttt{T.$s$}.
\end{itemize}
\why\ allows to open new namespaces explicitly in the text. In particular,
\why allows to open new namespaces explicitly in the text. In particular,
the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as:
\begin{verbatim}
......@@ -291,15 +291,15 @@ written as:
clone export Order
end
\end{verbatim}
However, since \why\ favours short theories over long and complex ones,
However, since \why favours short theories over long and complex ones,
this feature is rarely used.
\subsection{Example 2: Einstein's problem}
\index{Einstein's logic problem}
We now consider another, slightly more complex example: how to use \why\
We now consider another, slightly more complex example: how to use \why
to solve a little puzzle known as ``Einstein's logic
problem''\footnote{This \why\ example was contributed by St\'ephane Lescuyer.}.
problem''\footnote{This \why example was contributed by St\'ephane Lescuyer.}.
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
......@@ -444,7 +444,7 @@ theory Problem "Goal of Einstein's problem"
goal G: Pet.to Fish = German
end
\end{verbatim}
and we are ready to use \why\ to discharge this goal with any prover
and we are ready to use \why to discharge this goal with any prover
of our choice.
%%% Local Variables:
......
\chapter{Syntax Reference}
\label{chap:syntaxref}
This chapter gives the grammar for \why\ and \whyml\ input files.
This chapter gives the grammar for \why and \whyml input files.
\section{Lexical conventions}
Lexical conventions are common to \why\ and \whyml.
Lexical conventions are common to \why and \whyml.
% TODO: blanks
......@@ -54,6 +54,7 @@ characters they are built from:
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Why3 Language}
\paragraph{Terms.}
......@@ -135,23 +136,24 @@ $A~\verb|&&|~B$ into subgoals $A$ and $A\rightarrow B$.
\paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}.
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
\caption{Syntax for theories.}
\label{fig:bnf:theory}
\end{figure}
\paragraph{Files.}
A \why\ input file is a (possibly empty) list of theories.
A \why input file is a (possibly empty) list of theories.
\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\clearpage
\section{Why3ML Language}\label{sec:syntax:whyml}
\paragraph{Types.}
The syntax for program types is given in figure~\ref{fig:bnf:typev}.
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
\caption{Syntax for program types.}
\label{fig:bnf:typev}
......@@ -159,7 +161,7 @@ The syntax for program types is given in figure~\ref{fig:bnf:typev}.
\paragraph{Expressions.}
The syntax for program expressions is given in figure~\ref{fig:bnf:expr}.
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
\caption{Syntax for program expressions.}
\label{fig:bnf:expr}
......@@ -167,14 +169,14 @@ The syntax for program expressions is given in figure~\ref{fig:bnf:expr}.
\paragraph{Modules.}
The syntax for modules is given in figure~\ref{fig:bnf:module}.
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
\caption{Syntax for modules.}
\label{fig:bnf:module}
\end{figure}
\paragraph{Files.}
A \whyml\ input file is a (possibly empty) list of theories and modules.
A \whyml input file is a (possibly empty) list of theories and modules.
\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
......
\chapter{The Why3ML Programming Language}
\label{chap:whyml}
This chapter describes the \whyml\ programming language.
A \whyml\ input text contains a list of theories (see
This chapter describes the \whyml programming language.
A \whyml input text contains a list of theories (see
chapter~\ref{chap:syntax}) and/or modules.
Modules extend theories with \emph{programs}.
Programs can use all types, symbols, and constructs from the logic.
......
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