From f59baedf15008162842398e1e54cd8eadfbadb53 Mon Sep 17 00:00:00 2001
From: JeanChristophe Filliatre
Date: Mon, 29 Oct 2012 17:59:59 +0100
Subject: [PATCH] doc WhyML

doc/syntaxref.tex  256 +++++++++++++++++++++++
doc/whyml.tex  20 ++
2 files changed, 140 insertions(+), 136 deletions()
diff git a/doc/syntaxref.tex b/doc/syntaxref.tex
index 2cef65fc9..45351ce1e 100644
 a/doc/syntaxref.tex
+++ b/doc/syntaxref.tex
@@ 196,142 +196,142 @@ Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
\label{fig:bnf:exprb}
\end{figure}
In the following we describe the informal semantics of each
constructs, and provide the corresponding rule for computing the
weakest precondition.
+% In the following we describe the informal semantics of each
+% constructs, and provide the corresponding rule for computing the
+% weakest precondition.
\subsubsection{Constant Expressions, Unary and Binary Operators}
+% \subsubsection{Constant Expressions, Unary and Binary Operators}
Integer and real constants are as in the logic language, as weel as the unary and binary operators.
+% Integer and real constants are as in the logic language, as weel as the unary and binary operators.
\subsubsection{Array accesses and updates, fields access and updates}
+% \subsubsection{Array accesses and updates, fields access and updates}
\todo{}
+% \todo{}
\subsubsection{Let binding, sequences}

\todo{}

\subsubsection{Function definition}

\todo{fun, let rec}

\subsubsection{Function call}

\todo{}

\subsubsection{Exception throwing and catching}

\todo{raise, try with end}

\subsubsection{Conditional expression, pattern matching}

\todo{if then else. Discuss standard WP versus fast WP}

\subsubsection{Iteration Expressions}

There are three kind of expressions for iterating: bounded, unbounded and infinite.

\begin{itemize}
\item A bounded iteration has the form
\begin{flushleft}\ttfamily
 for $i$=$a$ to $b$ do invariant \{ $I$ \} $e$ done
\end{flushleft}
Expressions $a$ and $b$ are evaluated first and only once, then expression $e$ si evaluated successively for $i$ from $a$ to $b$ included. Nothing is executed if $a > b$. The invariant $I$ must hold at each iteration including before entering the loop and when leaving it. The rule for computing WP is as follows:
\begin{eqnarray*}
 WP(\texttt{for} \ldots, Q) &=& I(a) \land \\
&& \forall \vec{w} (\forall i, a \leq i \leq b \land I(i) \rightarrow WP(e,I(i+1))) \land (I(b+1) \rightarrow Q)
\end{eqnarray*}
where $\vec{w}$ is the set of references modified by $e$.

A downward bounded iteration is also available, under the form
\begin{flushleft}\ttfamily
 for $i$=$a$ downto $b$ do invariant \{ $I$ \} $e$ done
\end{flushleft}

\item An unbounded iteration has the form
\begin{flushleft}\ttfamily
 while $c$ do invariant \{ $I$ \} $e$ done
\end{flushleft}
it iterates the loop body $e$ until the condition $c$ becomes false.
\begin{eqnarray*}
 WP(\texttt{while} \ldots, Q) &=& I \land \\
&& \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q)
\end{eqnarray*}
where $\vec{w}$ is the set of references modified by $e$.

Additionally, such a loop can be given a variant $v$, a quantity that must decreases ar each iteration, so as to prove its termination.


\item An infinite iteration has the form
\begin{flushleft}\ttfamily
 loop invariant \{ $I$ \} $e$ end
\end{flushleft}
it iterates the loop forever, hence the only way to exit such a loop is to raise an exception.
\begin{eqnarray*}
 WP(\texttt{loop} \ldots, Q \mid Exc \Rightarrow R) &=& I \land \\
&& \forall \vec{w} (I \rightarrow WP(e,I)) \land (I \rightarrow WP(e,Exc \Rightarrow R))
\end{eqnarray*}
\end{itemize}

\subsubsection{Assertions, Code Contracts}

There are several form of expressions for inserting annotations in the code.
The first form of those are the \emph{assertions} which have the form
\begin{flushleft}\ttfamily
 \textsl{keyword} \{ \textsl{proposition} \}
\end{flushleft}
where \textsl{keyword} is either \texttt{assert}, \texttt{assume} or
\texttt{check}. They all state that the given proposition holds at the given program point. The differences are:
\begin{itemize}
\item \texttt{assert} requires to prove that the proposition holds, and then make it available in the context of the remaining of the code
\item \texttt{check} requires to prove that the proposition holds, but
 does not make it visible in the remaining
\item \texttt{assume} assumes that the proposition holds and make it
 visible in the context of the remaining code, without requiring to
 prove it. It acts like an axiom, but within a program.
\end{itemize}
The corresponding rules for computing WP are as follows:
\begin{eqnarray*}
 WP(\texttt{assert} \{ P \}, Q) &=& P \mathop{\&\&} Q = P \land (P \rightarrow Q)\\
 WP(\texttt{check} \{ P \}, Q) &=& P \land Q \\
 WP(\texttt{assume} \{ P \}, Q) &=& P \rightarrow Q
\end{eqnarray*}

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
 nondeterministic 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 does not check whether there exists any program
 that can effectively establish the postcondition (similarly as the
 introduction of a \texttt{val} at the global level).
\item $\texttt{abstract}~e~\{ Q \}$ makes sure that the evaluation of
 expression $e$ establishes the postcondition $Q$, and then abstract
 away the program state by the postcondition $Q$ (similarly to the
 \texttt{any} construct).
\end{itemize}
The corresponding rules for computing WP are as follows:
\[
\begin{array}{l}
 WP(\texttt{any}~\{ P \}~\tau~\epsilon~\{ Q \mid exn_i \Rightarrow R_i \} ,
 Q' exn_i \Rightarrow R'_i) = \\
 \qquad\qquad P \mathop{\&\&} \forall result, \epsilon.
 (Q \rightarrow Q') \land (R_i \rightarrow R'_i) \\
 WP(\texttt{abstract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
 Q' \mid exn_i \Rightarrow R'_i) = \\
 \qquad\qquad WP(e,Q \mid exn_i \Rightarrow R_i) \land
 \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
\end{array}
\]

\subsubsection{Labels, Operators \texttt{old} and \texttt{at}}

\todo{Labels, old, at}
+% \subsubsection{Let binding, sequences}
+
+% \todo{}
+
+% \subsubsection{Function definition}
+
+% \todo{fun, let rec}
+
+% \subsubsection{Function call}
+
+% \todo{}
+
+% \subsubsection{Exception throwing and catching}
+
+% \todo{raise, try with end}
+
+% \subsubsection{Conditional expression, pattern matching}
+
+% \todo{if then else. Discuss standard WP versus fast WP}
+
+% \subsubsection{Iteration Expressions}
+
+% There are three kind of expressions for iterating: bounded, unbounded and infinite.
+
+% \begin{itemize}
+% \item A bounded iteration has the form
+% \begin{flushleft}\ttfamily
+% for $i$=$a$ to $b$ do invariant \{ $I$ \} $e$ done
+% \end{flushleft}
+% Expressions $a$ and $b$ are evaluated first and only once, then expression $e$ si evaluated successively for $i$ from $a$ to $b$ included. Nothing is executed if $a > b$. The invariant $I$ must hold at each iteration including before entering the loop and when leaving it. The rule for computing WP is as follows:
+% \begin{eqnarray*}
+% WP(\texttt{for} \ldots, Q) &=& I(a) \land \\
+% && \forall \vec{w} (\forall i, a \leq i \leq b \land I(i) \rightarrow WP(e,I(i+1))) \land (I(b+1) \rightarrow Q)
+% \end{eqnarray*}
+% where $\vec{w}$ is the set of references modified by $e$.
+
+% A downward bounded iteration is also available, under the form
+% \begin{flushleft}\ttfamily
+% for $i$=$a$ downto $b$ do invariant \{ $I$ \} $e$ done
+% \end{flushleft}
+
+% \item An unbounded iteration has the form
+% \begin{flushleft}\ttfamily
+% while $c$ do invariant \{ $I$ \} $e$ done
+% \end{flushleft}
+% it iterates the loop body $e$ until the condition $c$ becomes false.
+% \begin{eqnarray*}
+% WP(\texttt{while} \ldots, Q) &=& I \land \\
+% && \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q)
+% \end{eqnarray*}
+% where $\vec{w}$ is the set of references modified by $e$.
+
+% Additionally, such a loop can be given a variant $v$, a quantity that must decreases ar each iteration, so as to prove its termination.
+
+
+% \item An infinite iteration has the form
+% \begin{flushleft}\ttfamily
+% loop invariant \{ $I$ \} $e$ end
+% \end{flushleft}
+% it iterates the loop forever, hence the only way to exit such a loop is to raise an exception.
+% \begin{eqnarray*}
+% WP(\texttt{loop} \ldots, Q \mid Exc \Rightarrow R) &=& I \land \\
+% && \forall \vec{w} (I \rightarrow WP(e,I)) \land (I \rightarrow WP(e,Exc \Rightarrow R))
+% \end{eqnarray*}
+% \end{itemize}
+
+% \subsubsection{Assertions, Code Contracts}
+
+% There are several form of expressions for inserting annotations in the code.
+% The first form of those are the \emph{assertions} which have the form
+% \begin{flushleft}\ttfamily
+% \textsl{keyword} \{ \textsl{proposition} \}
+% \end{flushleft}
+% where \textsl{keyword} is either \texttt{assert}, \texttt{assume} or
+% \texttt{check}. They all state that the given proposition holds at the given program point. The differences are:
+% \begin{itemize}
+% \item \texttt{assert} requires to prove that the proposition holds, and then make it available in the context of the remaining of the code
+% \item \texttt{check} requires to prove that the proposition holds, but
+% does not make it visible in the remaining
+% \item \texttt{assume} assumes that the proposition holds and make it
+% visible in the context of the remaining code, without requiring to
+% prove it. It acts like an axiom, but within a program.
+% \end{itemize}
+% The corresponding rules for computing WP are as follows:
+% \begin{eqnarray*}
+% WP(\texttt{assert} \{ P \}, Q) &=& P \mathop{\&\&} Q = P \land (P \rightarrow Q)\\
+% WP(\texttt{check} \{ P \}, Q) &=& P \land Q \\
+% WP(\texttt{assume} \{ P \}, Q) &=& P \rightarrow Q
+% \end{eqnarray*}
+
+% 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
+% nondeterministic 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 does not check whether there exists any program
+% that can effectively establish the postcondition (similarly as the
+% introduction of a \texttt{val} at the global level).
+% \item $\texttt{abstract}~e~\{ Q \}$ makes sure that the evaluation of
+% expression $e$ establishes the postcondition $Q$, and then abstract
+% away the program state by the postcondition $Q$ (similarly to the
+% \texttt{any} construct).
+% \end{itemize}
+% The corresponding rules for computing WP are as follows:
+% \[
+% \begin{array}{l}
+% WP(\texttt{any}~\{ P \}~\tau~\epsilon~\{ Q \mid exn_i \Rightarrow R_i \} ,
+% Q' exn_i \Rightarrow R'_i) = \\
+% \qquad\qquad P \mathop{\&\&} \forall result, \epsilon.
+% (Q \rightarrow Q') \land (R_i \rightarrow R'_i) \\
+% WP(\texttt{abstract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
+% Q' \mid exn_i \Rightarrow R'_i) = \\
+% \qquad\qquad WP(e,Q \mid exn_i \Rightarrow R_i) \land
+% \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
+% \end{array}
+% \]
+
+% \subsubsection{Labels, Operators \texttt{old} and \texttt{at}}
+
+% \todo{Labels, old, at}
\subsection{Modules}
diff git a/doc/whyml.tex b/doc/whyml.tex
index 0aa674ba6..8a4bebff0 100644
 a/doc/whyml.tex
+++ b/doc/whyml.tex
@@ 10,7 +10,10 @@ They also provide extra features:
\begin{itemize}
\item
In a record type declaration, some fields can be declared
 \texttt{mutable}.
+ \texttt{mutable} and/or \texttt{ghost}.
+\item
+ In an algebraic type declaration (this includes record types), an
+ invariant can be specified.
\item
There are programming constructs with no counterpart in the logic:
\begin{itemize}
@@ 19,6 +22,7 @@ They also provide extra features:
\item loops;
\item exceptions;
\item local and anonymous functions;
+ \item ghost parameters and ghost code;
\item annotations: pre and postconditions, assertions, loop invariants.
\end{itemize}
\item
@@ 182,7 +186,7 @@ module MaxAndSum
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 1.}
\label{fig:MaxAndSum}
\end{figure}
@@ 298,7 +302,7 @@ module InvertingAnInjection
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
\label{fig:Inverting}
\end{figure}
@@ 417,7 +421,7 @@ module SearchingALinkedList
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 3.}
\label{fig:LinkedList}
\end{figure}
@@ 582,7 +586,7 @@ module NQueens
False
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (1/2).}
\label{fig:NQueens1}
\end{figure}
@@ 728,7 +732,7 @@ automatically, including the verification of the lemmas themselves.
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (2/2).}
\label{fig:NQueens2}
\end{figure}
@@ 855,7 +859,7 @@ a one line code.
\end{whycode}
The code is given Figure~\ref{fig:AQueue}. The verification conditions
are all discharged automatically.
\begin{figure}
+\begin{figure}[p]
\centering
\begin{whycode}
module AmortizedQueue
@@ 901,7 +905,7 @@ module AmortizedQueue
= create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
end
\end{whycode}
\vspace*{2em}\hrulefill
+\vspace*{1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 5.}
\label{fig:AQueue}
\end{figure}

2.26.2