doc: macro \why now used everywhere (for Why3)

parent e08a91dc
\chapter{The Why3 Application Programming Interface}
\chapter{The \why\ Application Programming Interface}
\label{chap:api}
This chapter is a tutorial for the users who wants to link their own
OCaml code with the Why3 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
[TODO in Chapter~ref{chap:apidoc}.]
We assume the reader has a fair knowledge of the OCaml
language. Notice also that the Why3 library is installed: see
language. Notice also that the \why\ library is installed: see
Section~\ref{sec:installlib}.
......@@ -72,7 +72,7 @@ As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A and B -> A
\end{verbatim}
Notice that the concrete syntax of Why3 forbids predicate identifiers
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.
......@@ -94,7 +94,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 Why3 requires these symbol to be capitalized, but it is not
syntax of \why\ requires these symbol 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{Why3 command line tool}
\section{\why\ command line tool}
\section{IDE}
......
......@@ -3,8 +3,8 @@
\section{Architecture and Terminology}
Everything in Why3 revolves around the notion of
\emph{task}\index{task}. Why3, as a platform, is a tool that
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.
......@@ -26,13 +26,13 @@ TODO: continue
\section{Organization of this document}
This document is organized as follows. The first part, made of three chapters, provides tutorials to learn how to use Why3. The second part gathers reference
This document is organized as follows. The first part, made of three chapters, provides tutorials to learn how to use \why. The second part gathers reference
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 Why3 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,15 +43,15 @@ 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 Why3 programmatically,
Chapter~\ref{chap:api} presents how to use \why\ programmatically,
using the API. It is for the experimented users, who wants to link
Why3 library with their own code.
\why\ library with their own code.
Part 2 provides:
\begin{itemize}
\item In Chapter~\ref{chap:syntaxref}, the input syntax of files.
\item In Chapter~\ref{chap:library}, the standard library of
theories distributed with Why3.
theories distributed with \why.
\item In Chapter~\ref{chap:manpages}, the technical manual pages for the
tools of the platform. All tool options, and all the configuration
files are described in details there.
......
\chapter{Reference manuals for the Why3 tools}
\chapter{Reference manuals for the \why\ tools}
\label{chap:manpages}
\section{Compilation, Installation}
\label{sec:install}
Compilation of Why3 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}
......@@ -41,17 +41,17 @@ It is also installable from sources, available from the site
\subsection{Local use, without installation}
It is not mandatory to install Why3 to use it. Local use is obtained via
It is not mandatory to install \why\ to use it. Local use is obtained via
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
The Why3 executables are then available in subdirectory \texttt{bin/}.
The \why\ executables are then available in subdirectory \texttt{bin/}.
\subsection{Installation of the Why3 library}
\subsection{Installation of the \why\ library}
\label{sec:installlib}
By default, the Why3 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
......@@ -59,21 +59,21 @@ make install_lib
\section{Installation of external provers}
Why3 can use a wide range of external theorem provers. These need to
be installed separately, and then Why3 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 Why3 to use the provers, follow intructions given in
For configuring \why\ to use the provers, follow intructions given in
Section~\ref{sec:why3config}.
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
Why3 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
......@@ -86,7 +86,7 @@ of the IDE. This must be done again each time a new prover is installed.
The set of all provers which are attempted to detect is described in
the readable configuration file \texttt{provers-detection-data.conf}
of the Why3 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
......@@ -112,7 +112,7 @@ The provers which are typically attemped for detection are
\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 Why3
\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.
......@@ -126,7 +126,7 @@ provers and will replace them in the file configuration.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
Why3 is primarily used to call provers on goals contains by file in
\why\ is primarily used to call provers on goals contains by file in
why3 format \texttt{.why} extension. However plugins can register
parser which can extend the known format. \texttt{why3ml} apply the
following steps :
......@@ -163,7 +163,7 @@ following steps :
\end{enumerate}
\texttt{why3} call the prover sequentially, use \texttt{why3bench} if
you want to call the provers concurrently. \texttt{Why3} can also be
you want to call the provers concurrently. \why\ can also be
used to provide other informations :
\begin{itemize}
\item \texttt{print-namespace} print the namespace of the selected
......@@ -243,7 +243,7 @@ The preferences window allows you customize
\section{The \texttt{why3ml} tool}
The \texttt{why3ml} is an additional layer on Why3 library for
The \texttt{why3ml} is an additional layer on \why\ library for
generating verification conditions from WhyML programs. This tool and
the syntax of WhyML programs is intentionally left undocumented since
it might evolve significantly in the near future.
......
......@@ -86,8 +86,8 @@ $^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\chapter*{Foreword}
This is the manual for the Why platform version 3, or Why3 for
short. Why3 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. The major
change is a completely new design of the architecture for calling
external provers. An important emphasis is put on the genericity,
......@@ -98,11 +98,11 @@ to use Why programmatically, via a well-designed API.
\subsection*{Availability}
Why3 project page is \url{https://gforge.inria.fr/projects/why3}. The
\why\ project page is \url{https://gforge.inria.fr/projects/why3}. The
last distribution is available, in source format, together with this
documentation and several examples.
Why3 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
......@@ -114,13 +114,13 @@ 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 Why3 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}.
\section*{Acknowledgements}
We gratefully thank the people who contributed to Why3: Simon Cruanes,
We gratefully thank the people who contributed to \why: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\section*{Release notes}
......
......@@ -3,24 +3,24 @@
\section{Hello Proofs}
The first and basic step in using Why3 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 Why3 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} Any declaration must occur
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 Why3
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 Why3 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}).
......@@ -164,7 +164,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.
\section{Getting Started with the Why3 Command}
\section{Getting Started with the \why\ Command}
\label{sec:batch}
The why3 command allows to check the validity of goals with external
......
\chapter{Why3 Language}
\chapter{The \why\ Language}
\label{chap:syntax}
This chapter describes the input syntax, and informally gives its semantics,
......
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