Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit e4693ebb authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix some documentation typos.

parent 76141703
......@@ -12,7 +12,7 @@ small set of goals.
Any declaration must occur
inside a theory, which is in that example called HelloProof and
labelled with a comment inside double quotes. It contains three goals
labeled 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
requires to import the theory of integer arithmetic from the \why
......@@ -62,7 +62,7 @@ allows to browse inside the theories.
% all} or its shortcut \textsf{Ctrl-E}. This will result is something
% like the screenshot of Figure~\ref{fig:gui2}.
In this tree view, we have a structured view of the file: this file
contains one theory, itself containg three goals.
contains one theory, itself containing three goals.
\begin{figure}[tbp]
......
......@@ -261,13 +261,13 @@ The corresponding rules for computing WP are as follows:
The other forms of code contracts allow to abstract a piece of code by specifications.
\begin{itemize}
\item $\texttt{any}~\{ P \}~\tau~\epsilon~\{ Q \}$ is a
non-deterministic expression which requires the precondition $P$ to
hold, then makes some side effects $\epsilon$ and returns any value
non-deterministic expression that requires the precondition $P$ to
hold, then makes some side effects $\epsilon$, and returns any value
of type $\tau$ such that $Q$ holds. This construct acts as an axiom
in the sense that it is not check whether there exists any program
in the sense that it does not check whether there exists any program
that can effectively establish the post-condition (similarly as the
introduction of a \texttt{val} at the global level).
\item $\texttt{contract}~e~\{ Q \}$ evaluates expression $e$ and the
\item $\texttt{contract}~e~\{ Q \}$ evaluates the expression $e$ and
ensures that the post-condition $Q$ holds afterwards.
\item $\texttt{abstract}~e~\{ Q \}$ makes sure that the evaluation of
expression $e$ establishes the post-condition $Q$, and then abstract
......
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