diff --git a/doc/phd-project-2009-07/bib.bib b/doc/phd-project-2009-07/bib.bib
index 79c5fc4ea706b5078b9d453705c9cde8413b58b4..fabf9f39a743e2eab988791a1d44510d88daee05 100644
--- a/doc/phd-project-2009-07/bib.bib
+++ b/doc/phd-project-2009-07/bib.bib
@@ -24,9 +24,16 @@
year=2006
}
+@techreport{burak06mop,
+ title={{M}atching {O}bjects with {P}atterns},
+ author={Emir, Burak and Odersky, Martin and Williams, John},
+ year={2006},
+ unit={LAMP}
+}
+
@techreport{dotta08pm,
author={Dotta, Mirco and Suter, Philippe and Kuncak, Viktor},
- title={On {V}erifying {E}xpressive {P}attern {M}atching},
+ title={On {S}tatic {A}nalysis for {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 a3d43ed292b80f3aad014de36c149f3f6965993b..712e5b82c46804ff49de38993601c4a877383267 100644
--- a/doc/phd-project-2009-07/challenges.tex
+++ b/doc/phd-project-2009-07/challenges.tex
@@ -1 +1,2 @@
\section{Reasoning}
+
diff --git a/doc/phd-project-2009-07/code/beautify.sh b/doc/phd-project-2009-07/code/beautify.sh
index ec9dcef708dabb78e9e66aab20aab4effee78d83..25c729ae8d8dbdaa9b1822f144ea77ada59f8a0f 100755
--- a/doc/phd-project-2009-07/code/beautify.sh
+++ b/doc/phd-project-2009-07/code/beautify.sh
@@ -6,6 +6,8 @@ for src in *.scala ; do
cat ${src} | \
sed -e "s/==>/$\\\\rightarrow$/g" | \
sed -e "s/=>/$\\\\Rightarrow$/g" | \
+ sed -e "s/<=/$\\\\leq$/g" | \
+ sed -e "s/>=/$\\\\geq$/g" | \
sed -e "s/!=/$\\\\neq$/g" |
sed -e "s/==/=/g" |
cat > ${src}.cute
diff --git a/doc/phd-project-2009-07/commands.tex b/doc/phd-project-2009-07/commands.tex
index c4b0fb6bd6a298b32bd8e08989e6a1a234d3fbc2..f59a443ad32b143157d39849a903b38be50ddcf1 100644
--- a/doc/phd-project-2009-07/commands.tex
+++ b/doc/phd-project-2009-07/commands.tex
@@ -1,2 +1,3 @@
\newcommand{\purescala}{\textsf{f}Scala}
+\newcommand{\K}[1]{\textsf{#1}}
diff --git a/doc/phd-project-2009-07/examples.tex b/doc/phd-project-2009-07/examples.tex
index 9cf7bc95d0561954d62fa3f3b412cb64104b05c5..1a75c1add94dc0c67364fcca3df47b562b1060f6 100644
--- a/doc/phd-project-2009-07/examples.tex
+++ b/doc/phd-project-2009-07/examples.tex
@@ -1,6 +1,7 @@
-\section{Examples}
+\subsection{An Example}
Figure~\ref{fig:listset} shows an example program; a set data-structure
-implemented using a linked list.
+implemented using a linked list, along with some specifications about the
+implemented functions.
\begin{figure}
\lstinputlisting{code/ListSet.scala.cute}
@@ -8,3 +9,10 @@ implemented using a linked list.
\label{fig:listset}
\end{figure}
+One can note that in our example, the function \K{content} really plays
+the role of an abstraction function over the implementation. This
+(executable) function is then used very naturally in other contracts
+specifying for instance that \K{insert} is an operation compatible with
+the congruence relation defined by \K{content($a$) = content($b$)}. Such
+specifications would be either very unnaturally expressed using only pre-
+and post- conditions, or not expressible at all.
diff --git a/doc/phd-project-2009-07/future.tex b/doc/phd-project-2009-07/future.tex
index 5377e6eda4dd6a59aba03688d711b9daa10c6560..02b12c8dde3e0cfc7a3c82c1df94760c0de41db9 100644
--- a/doc/phd-project-2009-07/future.tex
+++ b/doc/phd-project-2009-07/future.tex
@@ -1,4 +1,20 @@
\section{Future Work}
+\paragraph{Implementation}
+The natural next step is to finish our implementation. This involves several
+challenges, some purely technical, such as dealing with the internal structure
+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
+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
+different \emph{view} on the same data. Supporting extractors and universally
+quantified specifications over them would allow us to superseed some of our
+previous work \cite{dotta08pm}.
-- extractors, superseeding \cite{dotta08pm}.
+In the longer term, we would like to keep {\purescala} as our specification
+language, but start extending the verified language. Some of the features we
+want to add include standard classes with mutable fields and comparison by
+reference.
diff --git a/doc/phd-project-2009-07/introduction.tex b/doc/phd-project-2009-07/introduction.tex
index 250fe6eefbc9b4162e1426abb64f99a940933b6a..822af61718fb6d689ddefbcce48e4791f555a3be 100644
--- a/doc/phd-project-2009-07/introduction.tex
+++ b/doc/phd-project-2009-07/introduction.tex
@@ -34,4 +34,12 @@ 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.
+high for a programmer to always copy a function body in its post-condition, and
+this would defeat the purpose of have specifications, which are supposed to
+provide an abstraction mechanism for the computations taking place in the
+functions. To give contracts additional expressive power, our system allows
+universally quantified global specifications.
+
+The rest of this report is as follows: the next section describes
+{\purescala}, the third one an example of a proof in the system, then we
+give an overview of the implementation status and describe future work.
diff --git a/doc/phd-project-2009-07/purescala.tex b/doc/phd-project-2009-07/purescala.tex
index 1047b7f2ace4519b07a749caebfce9401dcf8a45..b260acfb89dadf0c45de3937b47d91fe602769d4 100644
--- a/doc/phd-project-2009-07/purescala.tex
+++ b/doc/phd-project-2009-07/purescala.tex
@@ -1,22 +1,96 @@
\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.
+verification system, as well as the programming language under consideration
+in its first version. As mentioned previously, {\purescala} is purely
+functional: computations have no side effects. All features, including the
+concrete syntax, are taken from Scala or added as part of a minimalistic
+library, and as a result, any valid {\purescala} program is a valid Scala
+program as well\footnote{Provided the inclusion of our small library, that
+is.}, and can be compiled and executed using {\tt scalac} and {\tt scala}.
+When displaying code examples, for reasons of space and clarity, we sometimes
+replace elements of the concrete syntax by shorter versions (printing $\neq$
+instead of \K{!=}, for instance). It particular, since there are no assignments
+in {\purescala}, we always print $=$ instead of \K{==}, with no risk of
+confusion. All object-oriented features of Scala are kept out {\purescala}:
+there are no classes (expect for case classes, but with the restrictions we
+impose on them, they really just become immutable records).
\subsection{Features}
-- data types
+\subsubsection{Primitive Types}
+The \K{Boolean} type is associated with the literals \K{true} and \K{false}
+and the usual operators ($\neg$, $\land$, $\lor$, $=$, $\neq$). There is also
+an additional binary operator $\rightarrow$ which we describe later. This
+type is also used as the basic type for assertions and contracts.
-- ``all in an object''
+The \K{Int} type represent 32-bit integers and comes with the standard set of
+arithmetic operators and relation symbols ($+$, $-$, $\cdot$, $/$, $=$,
+$\neq$, $<$, $\leq$, $>$, $\geq$). Integer constants can be written in any
+format defined in the Scala specification.
-- ignoring main method
+\subsubsection{Collection Types}
+The \K{Option[A]} parametric type represents collections of $0$ or $1$
+element. Just like any other parametric type of {\purescala}, it can be
+instantiated with any other {\purescala} type, but since there are no type
+variables, it has to be made concrete. Values of types \K{Option[A]} are
+constructed by using \K{Some(\ldots)} or \K{None}, with the semantics being
+that all \K{None} values (of the same type) are equal, \K{None} is never
+equal to a \K{Some} value, and \K{Some($v_1$)} equals \K{Some($v_2$)} if and
+only if \K{$v_1$} and \K{$v_2$} are of the same type and are equal according
+to the definition of equality on that type.
-\subsection{Specifications}
-- universally quantified specs
+The \K{List[A]} type is used to represent linked lists. Although lists are
+pointer-based data structures, the comparison of two lists is always done
+element-by-element, and never on the references.
+
+Sets are useful for abstracting the content of data structures and are
+available in {\purescala} through the use of the (parametric) Scala library
+class \K{scala.collection.immutable.Set} and its companion object. The expected
+constructors, operators and relation symbols ($\emptyset$, $\{ \ldots \}$,
+$\cup$, $\cap$, $\in$, $\subseteq$) are available in this class.
+
+Multisets are not a part of the Scala library, but we consider them to be part
+of {\purescala} for convenience. We have a concrete implementation of that
+class so in practice,{\purescala} programs using multisets can be compiled by
+importing the proper definition. The operations are similar to those on sets, with the addition of the multiplicity function and $\uplus$.
+
+The parametric type \K{Map[A,B]} is used to represent functional maps. Like the
+other data types, it is purely functional, so updating a map returns a new map.
+The operations on maps are insertion, deletion and lookup. Lookup returns an
+\K{Option} type.
+
+\subsubsection{Algebraic Data Types}
+An important feature of {\purescala} is the possibility to define recursive
+data types. They correspond to case classes in Scala with the additional
+restrictions that all class hierarchies should be sealed, that classes can not
+declare methods or fields that are not arguments to the constructor, and that
+they should not be type-parametric.
-Signature of the method used in $\forall-$assertions:
+\subsubsection{Expressions}
+An expression in {\purescala} is either a value of the types mentioned above
+expressed a literal, or returned by a call to a constructor or a function call,
+or the result of the evaluation of one of the two control-flow contructs;
+if-then-else expressions and pattern matching. If-then-else expressions work as
+in Scala, and the else branch is not optional. Pattern matching can be done on
+integers, booleans, option types and user-defined recursive data types.
+Patterns can be guarded by an additional boolean constraint.
+
+\subsubsection{Structure of Programs}
+For simplicity reasons, a {\purescala} program should be written entirely
+within one component, or \K{object} in Scala terminology. All function, type,
+and ``global'' value definitions therefore have the same lexical scope. An
+exception to this rule is the possibility to write a \K{main} function, which
+is ignored by the static analysis, yet useful for runtime evaluation.
+
+\subsection{Specifications}
+Specifications can be given in terms of pre- and post-conditions of functions,
+but as mentioned in the introduction, this is not the most interesting form of
+contracts for {\purescala}. We write global specifications by means of calls to
+\K{assert} placed at the top-level of the main component. The special method \K{forAll} works as a universal quantifier on {\purescala} types. Its signature is the following:
\lstinputlisting{code/forall-method.scala.cute}
-For intance, we display the following universally quantified specification:
+Its semantics are that \K{forAll[A](f: A $\Rightarrow$ Boolean)} is true if and
+only if \K{f} returns true for any argument of type \K{A}. It should be clear that we can write a predicate with multiple universal quantifications using \K{forAll} repeatedly in a nested way, however this can lead to lengthy expressions, so we write these in a shorter way. For instance, we display the following universally quantified specification:
\lstinputlisting{code/spec-long.scala.cute}
@@ -24,3 +98,17 @@ For intance, we display the following universally quantified specification:
\lstinputlisting{code/spec-short.scala.cute}
+It should be noted that these universally quantified assertions are strictly
+more expressive that contracts expressed as pre- and post-conditions. Indeed,
+consider a function \K{f($x_1$, \ldots, $x_n$)} with pre-condition \K{pre($x_1$,
+\ldots, $x_n$)} and post-condition \K{res $\Rightarrow$ post(res, $x_1$, \ldots,
+$x_n$)}, where \K{res} is a variable representing the result of the evaluation. Then the contracts can be rewritten as the universally quantified specification:
+
+\begin{lstlisting}
+$\forall$ $x_1$, ..., $x_n$ .
+ pre($x_1$, ..., $x_n$) $\rightarrow$ post(f($x_1$, ..., $x_n$), $x_1$, ..., $x_n$)
+\end{lstlisting}
+
+In contrast, pre- and post-conditions can not be used to reason about different
+executions, for example to state that two different functions applied to the
+same arguments always yield the same result.
diff --git a/doc/phd-project-2009-07/status.tex b/doc/phd-project-2009-07/status.tex
index 1f7211333487b58e2049497c1972ab3fef91baee..aec8836e70801a50ebe1998a77bd89bae222b4af 100644
--- a/doc/phd-project-2009-07/status.tex
+++ b/doc/phd-project-2009-07/status.tex
@@ -1,3 +1,6 @@
\section{Implementation Status}
-
-Not much done yet.
+Our implementation is still at an early stage. We have defined a representation
+for abstract syntax trees of {\purescala} programs, and have started working on
+a compiler plugin for {\tt scalac} which generates the proper AST from actual
+Scala trees, and rejects Scala programs which are not {\purescala}. No
+procedure for automated reasoning is yet implemented.