diff --git a/doc/phd-project-2009-07/bib.bib b/doc/phd-project-2009-07/bib.bib
index 5cc64162d1dc9ac59519a3797756d30c49b6e94d..79c5fc4ea706b5078b9d453705c9cde8413b58b4 100644
--- a/doc/phd-project-2009-07/bib.bib
+++ b/doc/phd-project-2009-07/bib.bib
@@ -16,3 +16,17 @@
year={1998},
month={September},
}
+
+@techreport{scalalang,
+ author={Odersky, Martin and Altherr, Philippe and Cremet, Vincent and Dragos, Iulian and Dubochet, Gilles and Emir, Burak and McDirmid, Sean and Micheloud, Stéphane and Mihaylov, Nikolay and Schinz, Michel and Spoon, Lex and Stenman, Erik and Zenger, Matthias},
+ title={An {O}verview of the {S}cala {P}rogramming {L}anguage (2nd {E}dition)},
+ unit={LAMP},
+ year=2006
+}
+
+@techreport{dotta08pm,
+ author={Dotta, Mirco and Suter, Philippe and Kuncak, Viktor},
+ title={On {V}erifying {E}xpressive {P}attern {M}atching},
+ unit={LARA},
+ year={2008}
+}
diff --git a/doc/phd-project-2009-07/challenges.tex b/doc/phd-project-2009-07/challenges.tex
index 7f7095f5e0ded97f1f60c6b07d9f691655c8252b..a3d43ed292b80f3aad014de36c149f3f6965993b 100644
--- a/doc/phd-project-2009-07/challenges.tex
+++ b/doc/phd-project-2009-07/challenges.tex
@@ -1 +1 @@
-\section{Main Challenges}
+\section{Reasoning}
diff --git a/doc/phd-project-2009-07/code/ListSet.scala b/doc/phd-project-2009-07/code/ListSet.scala
index 042882cd286861f60893e63219de8ae708f0e845..d614bca2f4a8aefa689c662ad6d33ad95eb0305d 100644
--- a/doc/phd-project-2009-07/code/ListSet.scala
+++ b/doc/phd-project-2009-07/code/ListSet.scala
@@ -1,10 +1,18 @@
import scala.collection.immutable.Set
-import funcheck.Specs.forall
+import funcheck.Specs.{`==>`,forAll}
object ListSet {
- assert(forall(
- (ls1: List[Int]) => forall(
- (ls2: List[Int] => )
+ $\forall$ x: Int, xs: List[Int] .
+ content(insert(x, xs)) = content(xs) + x
+
+ $\forall$ x: Int, xs: List[Int] .
+ content(delete(x, xs)) = content(xs) - x
+
+ $\forall$ xs: List[Int], ys: List[Int], z: Int .
+ content(xs) == content(ys) ==> content(insert(z, xs)) == content(insert(z, ys))
+
+ $\forall$ xs: List[Int], ys: List[Int], z: Int .
+ content(xs) == content(ys) ==> content(delete(z, xs)) == content(delete(z, ys))
def content(xs: List[Int]): Set[Int] = xs match {
case Nil => Set.empty
diff --git a/doc/phd-project-2009-07/code/beautify.sh b/doc/phd-project-2009-07/code/beautify.sh
index 632c4c32bb3521d9ebb36532ba62e481a3276667..ec9dcef708dabb78e9e66aab20aab4effee78d83 100755
--- a/doc/phd-project-2009-07/code/beautify.sh
+++ b/doc/phd-project-2009-07/code/beautify.sh
@@ -3,7 +3,10 @@
rm -f *.cute
for src in *.scala ; do
- sed -e "s/=>/$\\\\Rightarrow$/g" ${src} | \
+ cat ${src} | \
+ sed -e "s/==>/$\\\\rightarrow$/g" | \
+ sed -e "s/=>/$\\\\Rightarrow$/g" | \
sed -e "s/!=/$\\\\neq$/g" |
- sed -e "s/==/=/g" > ${src}.cute
+ sed -e "s/==/=/g" |
+ cat > ${src}.cute
done
diff --git a/doc/phd-project-2009-07/code/spec-long.scala b/doc/phd-project-2009-07/code/spec-long.scala
new file mode 100644
index 0000000000000000000000000000000000000000..917dbeb7f1a20f2d89c9d6bec3e4ef69cd780531
--- /dev/null
+++ b/doc/phd-project-2009-07/code/spec-long.scala
@@ -0,0 +1,7 @@
+assert(
+ forAll((xs: List[Int]) =>
+ forAll((ys: List[Int]) =>
+ forAll((z: Int) => {
+ (content(xs) == content(ys)) ==> (content(insert(z, xs)) == content(insert(z, ys)))
+ })))
+)
diff --git a/doc/phd-project-2009-07/code/spec-short.scala b/doc/phd-project-2009-07/code/spec-short.scala
new file mode 100644
index 0000000000000000000000000000000000000000..507bf0ae5130b3ad5feaf9170bf4562e49f80329
--- /dev/null
+++ b/doc/phd-project-2009-07/code/spec-short.scala
@@ -0,0 +1,2 @@
+$\forall$ xs: List[Int], ys: List[Int], z: Int .
+ content(xs) == content(ys) ==> content(insert(z, xs)) == content(insert(z, ys))
diff --git a/doc/phd-project-2009-07/commands.tex b/doc/phd-project-2009-07/commands.tex
index cb634567816eea5a65344cbf9280b9ed3e6b975d..c4b0fb6bd6a298b32bd8e08989e6a1a234d3fbc2 100644
--- a/doc/phd-project-2009-07/commands.tex
+++ b/doc/phd-project-2009-07/commands.tex
@@ -1,13 +1,2 @@
-\newcommand{\jahob}{\textsf{Jahob}}
-\newcommand{\stp}{STP}
-\newcommand{\smt}{SMT}
-\newcommand{\pstp}{p-STP}
-\newcommand{\guru}{\textsf{VEPAR}}
-\newcommand{\vepar}{\textsf{VEPAR}}
-\newcommand{\formdecider}{\textsf{formDecider}}
-\newcommand{\hol}{HOL}
-\newcommand{\fol}{FOL}
-\newcommand{\todo}{\textsf{[TODO]}}
-\newcommand{\fstp}{$f$STP}
+\newcommand{\purescala}{\textsf{f}Scala}
-\newcommand{\K}[1]{\texttt{#1}}
diff --git a/doc/phd-project-2009-07/examples.tex b/doc/phd-project-2009-07/examples.tex
index e63d005358d24cf8124a04127300bebbdbecf42b..9cf7bc95d0561954d62fa3f3b412cb64104b05c5 100644
--- a/doc/phd-project-2009-07/examples.tex
+++ b/doc/phd-project-2009-07/examples.tex
@@ -1,3 +1,10 @@
\section{Examples}
+Figure~\ref{fig:listset} shows an example program; a set data-structure
+implemented using a linked list.
+\begin{figure}
\lstinputlisting{code/ListSet.scala.cute}
+\caption{A set implemented as a list in \purescala, along with universally quantified specifications.}
+\label{fig:listset}
+\end{figure}
+
diff --git a/doc/phd-project-2009-07/future.tex b/doc/phd-project-2009-07/future.tex
index d092f45b3411dabff32ec0d6a592501197510b14..5377e6eda4dd6a59aba03688d711b9daa10c6560 100644
--- a/doc/phd-project-2009-07/future.tex
+++ b/doc/phd-project-2009-07/future.tex
@@ -1,3 +1,4 @@
\section{Future Work}
-- extractors
+
+- extractors, superseeding \cite{dotta08pm}.
diff --git a/doc/phd-project-2009-07/introduction.tex b/doc/phd-project-2009-07/introduction.tex
index 6d8b74b859db56af880e6e0b5557c3d197fe1880..250fe6eefbc9b4162e1426abb64f99a940933b6a 100644
--- a/doc/phd-project-2009-07/introduction.tex
+++ b/doc/phd-project-2009-07/introduction.tex
@@ -1 +1,37 @@
\section{Introduction}
+Static software analysis systems typically work on source code annotated with
+specifications. The executable code is written in a programming language, and
+the annotations in a specification language. It is desirable for the latter to
+be easily comprehensible by the programmer, who, by definition, is an expert in
+the former. The design decisions which govern these languages are different,
+though: the programming language on the one hand, should allow the developer to
+efficiently describe computational processes, that is the algorithmic
+transformation of data. The specification language on the other hand should
+serve the purpose of describing relationships between data, for instance the
+relationship between a function arguments and its result, or between the
+results of two functions applied to the same arguments. (In a purely functional
+language, these two purposes become very close.) Additionally, the verification
+conditions eventually generated by the system should be expressed in a
+tractable logic, and that logic is closely tied to the choice of the
+specification language.
+
+Our long-term goal is the verification of programs written in the Scala
+programming language \cite{scalalang}, annotated with specifications written in
+a subset of Scala itself. Apart from the advantage that a user will be able to
+write these specifications as easily as the rest of his code, a second
+immediate benefit is that it will allow us to combine a test-based approach
+with our static analyses, since such specifications are executable. Finally,
+should both testing and static checking fail to convince a user that his
+program is conforming to its stated properties, the specifications will always
+be available for runtime checking, {\it \`a la} Eiffel. A natural choice for
+our specification language is a purely functional subset of Scala, which we
+call \purescala, and which we describe in the next section. As a first step in
+our long-term project, we will use \purescala\ as both the specification
+\emph{and} the programming language. That is, we will verify \purescala\
+programs annotated with \purescala\ specifications.
+
+This may appear to be a curious choice: indeed, if our specifications consisted
+only in pre- and post- conditions, as in most verification
+systems\footnote{Verification systems for object-oriented languages usually
+also have a mechanism to express class invariants.}, the temptation would be
+high for a programmer to always copy a function body in its post-condition.
diff --git a/doc/phd-project-2009-07/main.tex b/doc/phd-project-2009-07/main.tex
index 0d051a486d27f466fd9320be04cc52e91d4930f2..19899fe0f8afdacf0a4ecf95294b90971c385700 100644
--- a/doc/phd-project-2009-07/main.tex
+++ b/doc/phd-project-2009-07/main.tex
@@ -13,7 +13,7 @@
\title{Verification of Purely Functional Scala}
\author{Philippe Suter}
-
+\date{July 3, 2009} % hardcoded for the eventual satisfaction of our administration :)
\begin{document}
\maketitle
@@ -30,7 +30,7 @@
\input{future}
-\nocite{*}
+%\nocite{*}
\clearpage
\bibliographystyle{abbrv}
diff --git a/doc/phd-project-2009-07/purescala.tex b/doc/phd-project-2009-07/purescala.tex
index f731a0b41b5e1b8a26457fb120ad330b2e78bce7..1047b7f2ace4519b07a749caebfce9401dcf8a45 100644
--- a/doc/phd-project-2009-07/purescala.tex
+++ b/doc/phd-project-2009-07/purescala.tex
@@ -1,5 +1,26 @@
\section{A Purely Functional Subset of Scala}
+This section describes \purescala, the specification language of our
+verification system, as well as the programming language of its first version.
+
+\subsection{Features}
+- data types
+
+- ``all in an object''
+
+- ignoring main method
+
+\subsection{Specifications}
+- universally quantified specs
Signature of the method used in $\forall-$assertions:
\lstinputlisting{code/forall-method.scala.cute}
+
+For intance, we display the following universally quantified specification:
+
+\lstinputlisting{code/spec-long.scala.cute}
+
+\ldots as:
+
+\lstinputlisting{code/spec-short.scala.cute}
+
diff --git a/doc/phd-project-2009-07/status.tex b/doc/phd-project-2009-07/status.tex
index 9e7b50aa1da227d7cf5d991c49c7296f5d9fd6ce..1f7211333487b58e2049497c1972ab3fef91baee 100644
--- a/doc/phd-project-2009-07/status.tex
+++ b/doc/phd-project-2009-07/status.tex
@@ -1 +1,3 @@
\section{Implementation Status}
+
+Not much done yet.