From b3dd407d2d49043eef660accbc70e456c07ec36e Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 3 Jul 2009 20:48:59 +0000
Subject: [PATCH]
---
doc/phd-project-2009-07/bib.bib | 14 ++++++++
doc/phd-project-2009-07/challenges.tex | 2 +-
doc/phd-project-2009-07/code/ListSet.scala | 16 ++++++---
doc/phd-project-2009-07/code/beautify.sh | 7 ++--
doc/phd-project-2009-07/code/spec-long.scala | 7 ++++
doc/phd-project-2009-07/code/spec-short.scala | 2 ++
doc/phd-project-2009-07/commands.tex | 13 +------
doc/phd-project-2009-07/examples.tex | 7 ++++
doc/phd-project-2009-07/future.tex | 3 +-
doc/phd-project-2009-07/introduction.tex | 36 +++++++++++++++++++
doc/phd-project-2009-07/main.tex | 4 +--
doc/phd-project-2009-07/purescala.tex | 21 +++++++++++
doc/phd-project-2009-07/status.tex | 2 ++
13 files changed, 112 insertions(+), 22 deletions(-)
create mode 100644 doc/phd-project-2009-07/code/spec-long.scala
create mode 100644 doc/phd-project-2009-07/code/spec-short.scala
diff --git a/doc/phd-project-2009-07/bib.bib b/doc/phd-project-2009-07/bib.bib
index 5cc64162d..79c5fc4ea 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 7f7095f5e..a3d43ed29 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 042882cd2..d614bca2f 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 632c4c32b..ec9dcef70 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 000000000..917dbeb7f
--- /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 000000000..507bf0ae5
--- /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 cb6345678..c4b0fb6bd 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 e63d00535..9cf7bc95d 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 d092f45b3..5377e6eda 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 6d8b74b85..250fe6eef 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 0d051a486..19899fe0f 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 f731a0b41..1047b7f2a 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 9e7b50aa1..1f7211333 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.
--
GitLab