From 31f28050a1e32e99882a1bdb8ee05086c40980d9 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 6 Jul 2009 15:58:42 +0000
Subject: [PATCH]
---
doc/phd-project-2009-07/challenges.tex | 43 ++++++++++++++++++++++
doc/phd-project-2009-07/code/ListSet.scala | 2 +-
doc/phd-project-2009-07/future.tex | 2 +-
3 files changed, 45 insertions(+), 2 deletions(-)
diff --git a/doc/phd-project-2009-07/challenges.tex b/doc/phd-project-2009-07/challenges.tex
index 712e5b82c..bfbcf8989 100644
--- a/doc/phd-project-2009-07/challenges.tex
+++ b/doc/phd-project-2009-07/challenges.tex
@@ -1,2 +1,45 @@
\section{Reasoning}
+This section presents an example of proof of a specification. It should be
+noted that it does \emph{not} describe a general decision procedure for
+deciding the validity of such contracts. The mechanisms used are induction on
+data types (in this example, the primitive type of linked lists), and
+fold/unfold operations, that is inlining function calls and replacing
+expressions by equivalent function calls.
+We want to prove the third contract of Figure~\ref{fig:listset}:
+\begin{lstlisting}
+$\forall$ xs: List[Int], ys: List[Int], z: Int .
+ content(xs) = content(ys) $\rightarrow$ content(insert(z, xs)) = content(insert(z, ys))
+\end{lstlisting}
+
+We do it by induction on \K{xs}. For \K{xs = Nil}:
+\begin{lstlisting}
+content(Nil) = content(ys) $\rightarrow$ content(insert(z, Nil)) = content(insert(z, ys))
+\end{lstlisting}
+By unfolding \K{content(Nil)} and \K{insert(z, Nil)} we get:
+\begin{lstlisting}
+Set.empty = content(ys) $\rightarrow$ content(z :: Nil) = content(insert(z, ys))
+\end{lstlisting}
+By folding \K{content(ys)}, we get that for the left hand side to be true, we need \K{ys} to be \K{Nil}. We thus have:
+\begin{lstlisting}
+Set.empty = Set.empty $\rightarrow$ content(z :: Nil) = content(insert(z, Nil))
+\end{lstlisting}
+\ldots and by unfolding \K{insert} and \K{content} we get to the correct statement:
+\begin{lstlisting}
+Set.empty = Set.empty $\rightarrow$ Set(z) = Set(z)
+\end{lstlisting}
+
+Now for the case where \K{x = x' :: xs'}, \K{y = y' :: ys'}, assuming
+that the statement holds for \K{xs'} and \K{ys'}:
+\begin{lstlisting}
+content(x' :: xs') = content(y' :: ys') $\rightarrow$ content(insert(z, x' :: xs')) = content(insert(z, y' :: ys'))
+\end{lstlisting}
+We unfold \K{content} and \K{insert}:
+\begin{lstlisting}
+content(xs') + x = content(ys') + y $\rightarrow$ content(z :: x' :: xs')) = content(z :: y' :: ys'))
+\end{lstlisting}
+We unfold \K{content} again:
+\begin{lstlisting}
+content(xs') + x = content(ys') + y $\rightarrow$ content(xs') + x' + z = content(ys') + y' + z
+\end{lstlisting}
+\ldots and the statement is clearly true.
diff --git a/doc/phd-project-2009-07/code/ListSet.scala b/doc/phd-project-2009-07/code/ListSet.scala
index d614bca2f..fb2c51373 100644
--- a/doc/phd-project-2009-07/code/ListSet.scala
+++ b/doc/phd-project-2009-07/code/ListSet.scala
@@ -19,7 +19,7 @@ object ListSet {
case x :: xs => content(xs) + x
}
- def insert(x: Int, xs: List[Int]): List[Int] = if(member(x, xs)) xs else insert(x, xs)
+ def insert(x: Int, xs: List[Int]): List[Int] = x :: xs
def remove(x: Int, xs: List[Int]): List[Int] = xs match {
case Nil => Nil
diff --git a/doc/phd-project-2009-07/future.tex b/doc/phd-project-2009-07/future.tex
index 02b12c8dd..fe823f454 100644
--- a/doc/phd-project-2009-07/future.tex
+++ b/doc/phd-project-2009-07/future.tex
@@ -6,7 +6,7 @@ of {\tt scalac}, other more theoretical, such as how to automate fold/unfold
reasoning techniques.
\paragraph{Extension of {\purescala}}
-We would like to support \emph{extractors} \cite{burak06mop}in {\purescala}. Extractors are user
+We would like to support \emph{extractors} \cite{burak06mop} in {\purescala}. Extractors are user
defined functions to perform pattern-matching on recursive data types using a
different construction mechanism that the standard one consisting on matching
on the constructor arguments. To use a different terminology, they provide a
--
GitLab