intro.tex 2.26 KB
Newer Older
 MARCHE Claude committed Sep 08, 2010 1 2 3  \chapter{Introduction}  MARCHE Claude committed Sep 10, 2010 4 5 6 \section{Architecture and Terminology} Everything in Why3 revolves around the notion of  MARCHE Claude committed Oct 28, 2010 7 \emph{task}\index{task}. Why3, as a platform, is a tool that  MARCHE Claude committed Sep 10, 2010 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 committed Sep 08, 2010 24   MARCHE Claude committed Oct 28, 2010 25 26 TODO: continue  MARCHE Claude committed Sep 08, 2010 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 committed Dec 13, 2010 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 committed Sep 08, 2010 40   MARCHE Claude committed Oct 28, 2010 41 Chapter~\ref{chap:library} documents the standard library of theories  MARCHE Claude committed Dec 13, 2010 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 committed Oct 28, 2010 49   MARCHE Claude committed Sep 08, 2010 50 Chapter~\ref{chap:api} presents how to use Why3 programmatically,  MARCHE Claude committed Oct 28, 2010 51 52 using the API. It is for the experimented users, who wants to link Why3 library with their own code.  MARCHE Claude committed Sep 08, 2010 53   MARCHE Claude committed Oct 28, 2010 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 committed Sep 08, 2010 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: