diff --git a/doc/syntaxref.tex b/doc/syntaxref.tex index 2cef65fc94803a38d9aec0ba84139e54d078f6ef..45351ce1eb15529d46bdf9070ecfdc69c449ac48 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 - 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} diff --git a/doc/whyml.tex b/doc/whyml.tex index 0aa674ba63518b6e1bea48df6776a2d02c69e6de..8a4bebff055e6faaa3be5dca3875fd41a6eb3faa 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}