Skip to content
Snippets Groups Projects
Commit 6615dfc2 authored by Philippe Suter's avatar Philippe Suter
Browse files

No commit message

No commit message
parent 22426e3e
No related branches found
No related tags found
No related merge requests found
...@@ -24,9 +24,16 @@ ...@@ -24,9 +24,16 @@
year=2006 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, @techreport{dotta08pm,
author={Dotta, Mirco and Suter, Philippe and Kuncak, Viktor}, 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}, unit={LARA},
year={2008} year={2008}
} }
\section{Reasoning} \section{Reasoning}
...@@ -6,6 +6,8 @@ for src in *.scala ; do ...@@ -6,6 +6,8 @@ for src in *.scala ; do
cat ${src} | \ cat ${src} | \
sed -e "s/==>/$\\\\rightarrow$/g" | \ sed -e "s/==>/$\\\\rightarrow$/g" | \
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/!=/$\\\\neq$/g" |
sed -e "s/==/=/g" | sed -e "s/==/=/g" |
cat > ${src}.cute cat > ${src}.cute
......
\newcommand{\purescala}{\textsf{f}Scala} \newcommand{\purescala}{\textsf{f}Scala}
\newcommand{\K}[1]{\textsf{#1}}
\section{Examples} \subsection{An Example}
Figure~\ref{fig:listset} shows an example program; a set data-structure 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} \begin{figure}
\lstinputlisting{code/ListSet.scala.cute} \lstinputlisting{code/ListSet.scala.cute}
...@@ -8,3 +9,10 @@ implemented using a linked list. ...@@ -8,3 +9,10 @@ implemented using a linked list.
\label{fig:listset} \label{fig:listset}
\end{figure} \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.
\section{Future Work} \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.
...@@ -34,4 +34,12 @@ This may appear to be a curious choice: indeed, if our specifications consisted ...@@ -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 only in pre- and post- conditions, as in most verification
systems\footnote{Verification systems for object-oriented languages usually systems\footnote{Verification systems for object-oriented languages usually
also have a mechanism to express class invariants.}, the temptation would be 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.
\section{A Purely Functional Subset of Scala} \section{A Purely Functional Subset of Scala}
This section describes \purescala, the specification language of our 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} \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} The \K{List[A]} type is used to represent linked lists. Although lists are
- universally quantified specs 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} \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} \lstinputlisting{code/spec-long.scala.cute}
...@@ -24,3 +98,17 @@ For intance, we display the following universally quantified specification: ...@@ -24,3 +98,17 @@ For intance, we display the following universally quantified specification:
\lstinputlisting{code/spec-short.scala.cute} \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.
\section{Implementation Status} \section{Implementation Status}
Our implementation is still at an early stage. We have defined a representation
Not much done yet. 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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment