intro.tex 2.26 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
\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.
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39
Chapter~\ref{chap:tools} explains how to use the various command line
tools and 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
MARCHE Claude committed
40

MARCHE Claude's avatar
docs  
MARCHE Claude committed
41
Chapter~\ref{chap:library} documents the standard library of theories
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45 46 47 48
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
docs  
MARCHE Claude committed
49

MARCHE Claude's avatar
MARCHE Claude committed
50
Chapter~\ref{chap:api} presents how to use Why3 programmatically,
MARCHE Claude's avatar
docs  
MARCHE Claude committed
51 52
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
53

MARCHE Claude's avatar
docs  
MARCHE Claude committed
54 55 56
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
57 58 59 60 61 62 63 64 65 66

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



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