No commit message

No commit message

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}
+}

doc/phd-project-2009-07/challenges.tex

-\section{Main Challenges}
+\section{Reasoning}

doc/phd-project-2009-07/code/ListSet.scala

 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

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

doc/phd-project-2009-07/code/spec-long.scala

+assert(
+  forAll((xs: List[Int]) =>
+  forAll((ys: List[Int]) =>
+  forAll((z: Int) => {
+    (content(xs) == content(ys)) ==> (content(insert(z, xs)) == content(insert(z, ys)))
+  })))
+)

doc/phd-project-2009-07/code/spec-short.scala

+$\forall$ xs: List[Int], ys: List[Int], z: Int .
+  content(xs) == content(ys) ==> content(insert(z, xs)) == content(insert(z, ys))

doc/phd-project-2009-07/commands.tex

-\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}}

doc/phd-project-2009-07/examples.tex

 \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}
+

doc/phd-project-2009-07/future.tex

 \section{Future Work}
 
-- extractors
+
+- extractors, superseeding \cite{dotta08pm}.

doc/phd-project-2009-07/introduction.tex

 \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.

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}

doc/phd-project-2009-07/purescala.tex

 \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}
+

doc/phd-project-2009-07/status.tex

 \section{Implementation Status}
+
+Not much done yet.