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

\chapter{Introduction}

4 5 6
\section{Architecture and Terminology}

Everything in Why3 revolves around the notion of
MARCHE Claude's avatar
docs  
MARCHE Claude committed
7
\emph{task}\index{task}.  Why3, as a platform, is a tool that
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
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 
\begin{itemize}
\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
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
24

MARCHE Claude's avatar
docs  
MARCHE Claude committed
25 26
TODO: continue

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33 34 35 36 37 38 39
\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.

MARCHE Claude's avatar
docs  
MARCHE Claude committed
40 41 42 43 44 45
Chapter~\ref{chap:library} documents the standard library of theories
distributed with Why3. Chapter~\ref{chap:whyml} presents the
verification condition generator built upon the Why3 core.  The two
next chapters are for users with a little more experience, in
particular those who wants to use Why for verification of algorithms.

MARCHE Claude's avatar
MARCHE Claude committed
46
Chapter~\ref{chap:api} presents how to use Why3 programmatically,
MARCHE Claude's avatar
docs  
MARCHE Claude committed
47 48
using the API.  It is for the experimented users, who wants to link
Why3 library with their own code.
MARCHE Claude's avatar
MARCHE Claude committed
49

MARCHE Claude's avatar
docs  
MARCHE Claude committed
50 51 52
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.
MARCHE Claude's avatar
MARCHE Claude committed
53 54 55 56 57 58 59 60 61 62

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



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