manual.tex 1.87 KB
 MARCHE Claude committed Sep 03, 2010 1 2 \documentclass[a4paper]{memoir}  MARCHE Claude committed Sep 08, 2010 3 \usepackage[T1]{fontenc}  MARCHE Claude committed Sep 07, 2010 4 \usepackage{url}  MARCHE Claude committed Sep 07, 2010 5   MARCHE Claude committed Sep 08, 2010 6 7 % for ocamldoc generated pages \usepackage{ocamldoc}  MARCHE Claude committed Sep 07, 2010 8 9 \let\tt\ttfamily \let\bf\bfseries  MARCHE Claude committed Sep 07, 2010 10   MARCHE Claude committed Sep 08, 2010 11   MARCHE Claude committed Sep 03, 2010 12 13 \begin{document}  MARCHE Claude committed Sep 08, 2010 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 \thispagestyle{empty} \begin{center} ~ \vfill {\Huge\bfseries Why3 manual} \vfill {\Large F. Bobot$^{1,2}$ \\ J.-C. Filli\^atre$^{2,1}$ \\ C. March\'e$^{3,1}$ \\ A. Paskevich$^{1,2}$} \vfill \begin{tabular}{l} $^1$ Univ Paris-Sud, Orsay, F-91405 \\ $^2$ LRI, CNRS, Orsay, F-91405 \\ $^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893 \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 51 52 53 54 55  \cleardoublepage \tableofcontents  MARCHE Claude committed Sep 08, 2010 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 \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 external prover if wanted. An major new feature is also the ability to use Why programmatically, via an well-defined API. \section*{Acknowledgements} We gratefully thank all the people who contributed to this document:  MARCHE Claude committed Sep 08, 2010 71 72 \input{intro.tex}  MARCHE Claude committed Sep 06, 2010 73 \input{syntax.tex}  MARCHE Claude committed Sep 03, 2010 74 75 76  \input{ide.tex}  MARCHE Claude committed Sep 06, 2010 77 78 79 80 \input{api.tex} \input{manpages.tex}  MARCHE Claude committed Sep 07, 2010 81 \chapter{Complete API documentation}  MARCHE Claude committed Sep 08, 2010 82 \label{chap:apidoc}  MARCHE Claude committed Sep 07, 2010 83 84 85  \input{./apidoc.tex}  MARCHE Claude committed Sep 08, 2010 86 87 88 \bibliographystyle{abbrv} \bibliography{manual}  MARCHE Claude committed Sep 03, 2010 89 \end{document}  MARCHE Claude committed Sep 06, 2010 90 91 92 93 94 95  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: t %%% End:`