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

\chapter{Introduction}

4 5
\section{Architecture and Terminology}

MARCHE Claude's avatar
MARCHE Claude committed
6
Everything in \why revolves around the notion of
7
\emph{task}\index{task}.  \why, as a platform, is a tool that
8 9 10 11
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
MARCHE Claude's avatar
MARCHE Claude committed
12
(\ie a \emph{logical sequent} with exactly one formula in the
13 14 15 16 17 18 19 20 21 22 23
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

25
% \todo{continue}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
26

MARCHE Claude's avatar
MARCHE Claude committed
27 28
\section{Organization of this document}

29
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
MARCHE Claude's avatar
MARCHE Claude committed
30 31
manuals, giving detailed technical informations.

32 33
Chapter~\ref{chap:starting} explains how to use the GUI
for visualizing theories and goals, calling external provers for
MARCHE Claude's avatar
MARCHE Claude committed
34
trying to solve them, and applying transformations to simplify
MARCHE Claude's avatar
MARCHE Claude committed
35
them. It also presents the basic use of \why in
MARCHE Claude's avatar
MARCHE Claude committed
36
batch. Chapter~\ref{chap:syntax} presents the input syntax for file
37
defining \why theories. The semantics is given informally with
MARCHE Claude's avatar
MARCHE Claude committed
38
examples.  The two first chapters are thus to read for the beginners.
MARCHE Claude's avatar
MARCHE Claude committed
39

MARCHE Claude's avatar
MARCHE Claude committed
40 41 42 43 44
%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
45

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

MARCHE Claude's avatar
MARCHE Claude committed
50 51 52
Part 2 provides: 
\begin{itemize}
\item In Chapter~\ref{chap:syntaxref}, the input syntax of files.
53 54
% \item In Chapter~\ref{chap:library}, the standard library of
%   theories distributed with \why.
MARCHE Claude's avatar
MARCHE Claude committed
55 56 57
\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.
MARCHE Claude's avatar
MARCHE Claude committed
58
% \item In Chapter~\ref{chap:apidoc}, the technical documentation of the API.
MARCHE Claude's avatar
MARCHE Claude committed
59
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63 64 65 66


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