Commit bfb91d48 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Review the start of documentation.

parent 25378692
......@@ -138,9 +138,8 @@ Report any bug to the \why Bug Tracking System:
\subsection*{Acknowledgements}
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Johannes Kanig, St\'ephane
Lescuyer, Sim\~ao Melo de Sousa, Guillaume Melquiond, Benjamin Monate,
Asma Tafat.
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
\subsection*{Summary of Changes w.r.t. Why 2}
......@@ -154,7 +153,7 @@ are the following.
\item recursive definitions of logic functions and predicates, with
termination checking
\item inductive definitions of predicates
\item declarations are structured in components called "theories",
\item declarations are structured in components called ``theories'',
which can be reused and instantiated
\end{itemize}
......@@ -164,10 +163,11 @@ are the following.
\item generic concept of task transformation
\item generic approach for communicating with external provers
\end{itemize}
\item Source code organized as a library with a documented API, to
allow access to \why features programmatically.
\item GUI with new features w.r.t. the former GWhy
\item GUI with new features with respect to the former GWhy
\begin{itemize}
\item session save and restore
\item prover calls in parallel
......@@ -176,6 +176,7 @@ are the following.
\item ability to edit proofs for interactive provers (Coq only for
the moment) on any subtask
\end{itemize}
\item Extensible architecture via plugins
\begin{itemize}
\item users can define new transformations
......
......@@ -3,17 +3,15 @@
\section{Hello Proofs}
The first and basic step in using \why is to write a suitable input
file. When one wants to learn a programming language, you start by
writing a basic program. Here we start by writing a file containing a
basic set of goals.
Here is our first \why file, which is the file
\texttt{examples/hello\_proof.why} of the distribution.
The first step in using \why is to write a suitable input
file. When one wants to learn a programming language, one starts by
writing a basic program. Here is our first \why file, which is the file
\texttt{examples/hello\_proof.why} of the distribution. It contains a
small set of goals.
\lstinputlisting[language=why3]{../examples/hello_proof.why}
Any declaration must occur
inside a theory, which is in that example called TheoryProof and
inside a theory, which is in that example called HelloProof and
labelled with a comment inside double quotes. It contains three goals
named $G_1,G_2,G_3$. The first two are basic propositional goals,
whereas the third involves some integer arithmetic, and thus it
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment