intro.tex 1.87 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3


4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
\section{Architecture and Terminology}

Everything in Why3 revolves around the notion of
\emph{task}\index{task}.  Why3, as a platform, as a tool that
translates its input to a number of tasks, and dispatches these tasks
to external provers. 

Essentially, a task is a sequence of premises followed by a goal
(i.e.~a \emph{logical sequent} with exactly one formula in the
succedent). The language of tasks is based on first-order language
extended with 
\item polymorphic types;
\item algebraic types together with pattern matching;
\item definitions of functions and predicates, possibly recursive or
  mutually recursive;
\item inductively defined predicates;
\item \texttt{let} and \texttt{if-then-else} constructs;
%\item Hilbert's epsilon construct
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53

\section{Organization of this document}

This document is organized as follows. The first three chapters are
user manuals, to learn how to use Why3. Other chapters are reference
manuals, giving detailed technical informations.

Chapter~\ref{chap:syntax} presents the input syntax for file defining
Why theories. The semantics is given informally with examples.
Chapter~\ref{chap:ide} explains how to use the Why IDE for visualizing
theories and goals, call external provers for trying to solve them,
apply transformations to simplify them. The two first chapters are
thus to read for the beginners.

Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API.  It is for the more advanced users, who wants to link
Why3 library with their own code. 

Chapter~\ref{chap:manpages} are the technical manual pages for the tools of
the platform. All tool options, and all the configuration files are described in details there.

Chapter~\ref{chap:apidoc} is the technical documentation of the API.

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