intro.tex 2.45 KB
 MARCHE Claude committed Sep 08, 2010 1 2 3  \chapter{Introduction}  MARCHE Claude committed Sep 10, 2010 4 5 \section{Architecture and Terminology}  MARCHE Claude committed Jul 02, 2011 6 Everything in \why revolves around the notion of  Jean-Christophe Filliâtre committed Dec 17, 2010 7 \emph{task}\index{task}. \why, as a platform, is a tool that  MARCHE Claude committed Sep 10, 2010 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 committed Oct 10, 2013 12 (\ie a \emph{logical sequent} with exactly one formula in the  MARCHE Claude committed Sep 10, 2010 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 committed Sep 08, 2010 24   MARCHE Claude committed Oct 29, 2012 25 % \todo{continue}  MARCHE Claude committed Oct 28, 2010 26   MARCHE Claude committed Sep 08, 2010 27 28 \section{Organization of this document}  Jean-Christophe Filliâtre committed Dec 17, 2010 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 committed Sep 08, 2010 30 31 manuals, giving detailed technical informations.  MARCHE Claude committed Dec 15, 2010 32 33 34 Chapter~\ref{chap:starting} explains how to get started with the Why IDE for visualizing theories and goals, calling external provers for trying to solve them, and applying transformations to simplify  MARCHE Claude committed Jul 02, 2011 35 them. It also presents the basic use of \why in  MARCHE Claude committed Dec 15, 2010 36 37 38 batch. Chapter~\ref{chap:syntax} presents the input syntax for file defining Why theories. The semantics is given informally with examples. The two first chapters are thus to read for the beginners.  MARCHE Claude committed Sep 08, 2010 39   MARCHE Claude committed Dec 13, 2010 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 committed Oct 28, 2010 45   MARCHE Claude committed Jul 02, 2011 46 Chapter~\ref{chap:api} presents how to use \why programmatically,  MARCHE Claude committed Oct 28, 2010 47 using the API. It is for the experimented users, who wants to link  MARCHE Claude committed Jul 02, 2011 48 \why library with their own code.  MARCHE Claude committed Sep 08, 2010 49   MARCHE Claude committed Dec 15, 2010 50 51 52 Part 2 provides: \begin{itemize} \item In Chapter~\ref{chap:syntaxref}, the input syntax of files.  Jean-Christophe Filliâtre committed Feb 28, 2014 53 54 % \item In Chapter~\ref{chap:library}, the standard library of % theories distributed with \why.  MARCHE Claude committed Dec 15, 2010 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 committed Dec 16, 2010 58 % \item In Chapter~\ref{chap:apidoc}, the technical documentation of the API.  MARCHE Claude committed Dec 15, 2010 59 \end{itemize}  MARCHE Claude committed Sep 08, 2010 60 61 62 63 64 65 66  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: