intro.tex 1.11 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33

\chapter{Introduction}


\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.

Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API.  It is for the more advanced users, who wants to link
Why3 library with their own code. 

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.

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



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