doc WhyML

parent e8a744d1
......@@ -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
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 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{abstract}~e~\{ Q \}$ makes sure that the evaluation of
expression $e$ establishes the post-condition $Q$, and then abstract
away the program state by the post-condition $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
% 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 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{abstract}~e~\{ Q \}$ makes sure that the evaluation of
% expression $e$ establishes the post-condition $Q$, and then abstract
% away the program state by the post-condition $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}
......
......@@ -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}
......
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