manual.tex 2.13 KB
 MARCHE Claude committed Sep 14, 2010 1 \documentclass[a4paper,11pt,twoside,openright]{memoir}  MARCHE Claude committed Sep 03, 2010 2   MARCHE Claude committed Sep 08, 2010 3 \usepackage[T1]{fontenc}  MARCHE Claude committed Sep 14, 2010 4 5 %\usepackage{url} \usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}  MARCHE Claude committed Sep 07, 2010 6   Andrei Paskevich committed Dec 11, 2010 7 8 9 \usepackage[toc,nonumberlist]{glossaries} \makeglossaries  MARCHE Claude committed Sep 08, 2010 10 11 % for ocamldoc generated pages \usepackage{ocamldoc}  MARCHE Claude committed Sep 07, 2010 12 13 \let\tt\ttfamily \let\bf\bfseries  MARCHE Claude committed Sep 07, 2010 14   MARCHE Claude committed Sep 08, 2010 15   MARCHE Claude committed Sep 03, 2010 16 \begin{document}  MARCHE Claude committed Dec 08, 2010 17 18 \sloppy \hbadness=1100  MARCHE Claude committed Sep 03, 2010 19   MARCHE Claude committed Sep 08, 2010 20 21 22 23 24 25 26 27 28 29 30 31 \thispagestyle{empty} \begin{center} ~ \vfill {\Huge\bfseries Why3 manual} \vfill  Andrei Paskevich committed Dec 11, 2010 32 33 34 {\Large F. Bobot$^{1,2}$ \\ J.-C. Filli\^atre$^{2,1}$ \\ C. March\'e$^{3,1}$ \\  MARCHE Claude committed Sep 08, 2010 35 36 37 38 39 40 41 A. Paskevich$^{1,2}$} \vfill \begin{tabular}{l} $^1$ Univ Paris-Sud, Orsay, F-91405 \\ $^2$ LRI, CNRS, Orsay, F-91405 \\  Andrei Paskevich committed Dec 11, 2010 42 $^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893  MARCHE Claude committed Sep 08, 2010 43 44 45 46 47 48 49 50 51 52 53 54 55 56 \end{tabular} \vfill \begin{flushleft} \textcopyright 2010-2010 Univ Paris-Sud, CNRS, INRIA This work has been supported by the U3CAT' national ANR project (ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the Hi-Lite (\url{http://www.open-do.org/projects/hi-lite/}) FUI project of the System@tic competitivity cluster. \end{flushleft} \end{center}  MARCHE Claude committed Sep 06, 2010 57 58 59 60 61  \cleardoublepage \tableofcontents  MARCHE Claude committed Sep 08, 2010 62 63 64 65 66 67 68 69 \chapter*{Foreword} This is the manual for the Why platform version 3, or Why3 for short. Why3 is a complete reimplementation of the former Why platform~\cite{filliatre07cav} for program verification. The major change is a completely new design of the architecture for calling external provers. An important emphasis is put on the genericity, which allows for the end user to easily add the support for a new  MARCHE Claude committed Sep 10, 2010 70 71 external prover if wanted. A major new feature is also the ability to use Why programmatically, via a well-designed API.  MARCHE Claude committed Sep 08, 2010 72 73 74 75 76  \section*{Acknowledgements} We gratefully thank all the people who contributed to this document:  MARCHE Claude committed Sep 08, 2010 77 78 \input{intro.tex}  MARCHE Claude committed Sep 06, 2010 79 \input{syntax.tex}  MARCHE Claude committed Sep 03, 2010 80 81 82  \input{ide.tex}  MARCHE Claude committed Oct 28, 2010 83 84 85 86 \input{library.tex} \input{whyml.tex}  MARCHE Claude committed Sep 06, 2010 87 88 \input{api.tex}  Andrei Paskevich committed Dec 11, 2010 89 90 \input{glossary.tex}  MARCHE Claude committed Sep 06, 2010 91 92 \input{manpages.tex}  MARCHE Claude committed Sep 07, 2010 93 \chapter{Complete API documentation}  MARCHE Claude committed Sep 08, 2010 94 \label{chap:apidoc}  MARCHE Claude committed Sep 07, 2010 95 96 97  \input{./apidoc.tex}  MARCHE Claude committed Sep 08, 2010 98 \bibliographystyle{abbrv}  MARCHE Claude committed Oct 28, 2010 99 100 \bibliography{manual} %\input{biblio-demons}  MARCHE Claude committed Sep 10, 2010 101   MARCHE Claude committed Sep 03, 2010 102 \end{document}  MARCHE Claude committed Sep 06, 2010 103 104 105 106 107 108  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: t %%% End:`