% $Id: fmco.tex,v 1.42 2007/01/29 20:17:44 leavens Exp $
\documentclass{llncs}

\usepackage{verbatim}
% in fancyvrb, you can split input and number lines...
\usepackage{fancyvrb}
\usepackage{color}

\renewcommand{\textfraction}{0.15}
\renewcommand{\floatpagefraction}{0.66}

\def\old{\texttt{\char'134old}}
\def\result{\texttt{\char'134result}}
\def\everything{\texttt{\char'134everything}}
\def\nothing{\texttt{\char'134nothing}}

 \pagestyle{plain} % turn on pagenumbering - remove in final version
\begin{document}

\title{Beyond Assertions: 
       Advanced Specification and Verification with JML and ESC/Java2}

\author{Patrice Chalin\inst{1}
        \and Joseph R. Kiniry\inst{2}
        \and Gary T. Leavens\inst{3} 
        \and Erik Poll\inst{4}
       }


\institute{Concordia University, Montr\'eal, Qu\'ebec, Canada
           \and
           University College Dublin, Ireland
           \and
           Iowa State University,  Ames, Iowa, USA 
           \and 
           Radboud University Nijmegen, the Netherlands
          }

% ``Notes-to-authors''
% \newcommand{\NTA}[1]{\begin{quotation}\textsf{#1}\end{quotation}}
% \newcommand{\NTA}[1]{[NTA\footnote{#1}]}

%\newcommand{\COMMENT}[1]{{\sf\scriptsize  #1}}
%\newcommand{\MARGIN}[1]{\marginpar{\sf\scriptsize #1}}
\newcommand{\MARGIN}[1]{}
\newcommand{\COMMENT}[1]{}
\newcommand{\GMARGIN}[1]{\MARGIN{\textcolor{blue}{\sf\scriptsize #1}}}

\newcommand{\figref}[1]{\figurename~\ref{#1}}
\newcommand{\secref}[1]{Section~\ref{#1}}

\newcommand{\extracite}[1]{} % {\cite{#1}}

\newcommand{\todo}{\textbf{TODO:}}
\newcommand{\eg}{e.g.,\xspace}
\newcommand{\ie}{i.e.,\xspace}
\newcommand{\etc}{etc.\xspace}

\maketitle

\begin{abstract}
Many state-based specification languages, including the Java Modeling Language
(JML), contain at their core specification constructs familiar to most
undergraduates: e.g., assertions,
pre- and postconditions, and invariants.  Unfortunately, these constructs are
not sufficiently expressive to permit formal modular verification of programs
written in modern object-oriented languages like Java. The necessary extra
constructs for specifying an object-oriented module include (perhaps the less familiar)
frame properties, datagroups, and ghost and model fields.  These constructs
help specifiers deal with potential problems related to, for example, unexpected side
effects, aliasing, class invariants, inheritance, and lack of information
hiding.
%
This tutorial paper focuses on JML's realization of
these constructs, explaining their meaning while
illustrating how they can be used to address the stated problems.
\end{abstract}

\section{Introduction}

% [[[I'm surprised that there is no mention in the paper of the 
% non-null annotation that is shown in the examples, nor is 
% there any mention of whether JML is going to make that the 
% default or not.]]] -GTL

% This is now taken care of by Patrice's edits of 15 May, rev 1.34. -JRK

Textbooks on program 
verification~\extracite{Apt-Olderog97,Francez92,Loeckx-Sieber87} typically explain the
notions of pre- and postconditions, loop invariants, and so on for toy
programming languages.
%
The goal of this paper is to explain some of the more advanced concepts that
are necessary in order to allow the formal modular verification of
(sequential) programs written in a popular mainstream object-oriented
language: Java.
%
The Java Modeling Language 
(JML)~\cite{STTT05,Leavens-Baker-Ruby06,Leavens-etal06}, a Behavioral Interface
Specification Language (BISL)~\cite{Wing90a} for Java, will be our
notation of choice for expressing specifications.

The reader is assumed to be familiar with the basics of Design by
Contract (DBC)~\cite{Meyer97} or Behavioral Interface Specifications (BISs)
and the central role played by assertions in these approaches.
%
Readers without this background may wish to consult one of several
books or articles offering tutorials on the 
subject~\cite{Hoare69,Liskov-Guttag01,Mitchell-McKim02,Meyer92a,Meyer97,Morgan94}.
%
A tutorial that explains these basic ideas using JML is also 
available~\cite{Leavens-Cheon05}.

% Note that, as a tutorial, this paper does not present any new results.
% However, we believe that the ideas are of interest to the wider
% community of people interested in formal methods for object-oriented
% languages.

\subsection{Approaches to verification}
%
\MARGIN{Purpose (as far as I can tell --PC): mention tools support; introduce
  ESC/Java2 and motivate the need for the advanced features talked about in
  this paper (viz. without them static verification cannot be effective).}
%
% \MARGIN{FYI: I'm not sure why the content of this section is as it is.
%   I've revised it while kept the original focus on RAC vs. SV. Maybe we should
%   just talk about ``tool support'' in general :).  I can probably guess that
%   the section was originally motivated by the actual tutorial material in
%   which jmlc and ESC/Java2 are discussed, but we talk about neither of these
%   specifically in the paper, ... right? Well actually, we do talk about
%   ESC/Java2, but not jmlc. In any case I will leave the content as is for
%   now. --PC}

Tools useful for checking that JML annotated Java modules meet their
specifications fall into two main categories:%
%
\footnote{There are also several other kinds of tool available for use
  with JML~\cite{STTT05}.}
%
\begin{itemize}
  \item runtime assertion checking (RAC) tools, and
  \item static verification (SV) tools.
\end{itemize}
%
\MARGIN{Trim this sentence on origins? If we do, maybe remove reference to
  Rosenblum a few lines down? --PC}
These categories also represent two complementary forms of assertion checking, the
foundations of which were laid out before the 1950s in the pioneering work
of Goldstine, von Neumann and Turing~\cite{Jones03}.
%
% RAC:
Runtime assertion checking involves the testing of specifications during
program execution; any violations result in special errors being reported.
%
The idea of checking \emph{contracts} at runtime
was popularized by Eiffel~\cite{Meyer97} as of the late 80s; other early work includes
Rosenblum's APP annotation language for C~\cite{Rosenblum92,Rosenblum95}.
%% goes back to (at least) Rosenblum's work on 
%% APP~\cite{Rosenblum92,Rosenblum95}\MARGIN{A candidate for citation trim? --PC}
%% and was popularized by Eiffel~\cite{Meyer97}.
%
The main RAC tool for JML is \texttt{jmlc}~\cite{Cheon-Leavens02b}.
% Jass:
RAC support for JML is also planned for the next release of the Jass tool
\cite{Bartetzko-etal01}.

In static verification,
logical techniques are used to prove, before runtime, that no violations of
specifications will take place at runtime.
The adjective \emph{static\/} emphasizes that verification
happens by means of a static analysis of the code, i.e., without running it.
%
%% There are two main kinds of static verifiers:
%% \begin{itemize}
%%   \item Extended Static Checking (ESC) tools that perform efficient and fully
%%     automatic checking at the cost of being potentially unsound and
%%     incomplete,
%%   \item full program verification (PV) tools that are designed to be sound and
%%     complete, at the expense of requiring much more human intervention and
%%     insight during the verification process.
%% \end{itemize}
%
Program verification tools supporting JML include JACK~\cite{JACK}, KeY
\cite{KeY}, Krakatoa~\cite{Krakatoa}, LOOP~\cite{LOOP}, and Jive
\cite{Jive00}.  In this paper we will focus on ESC/Java2~\cite{Cok-Kiniry04},
the main (extended) static checker for JML.
% the successor tool to ESC/Java~\cite{Flanagan-Et-Al02}.

RAC and SV tools have complementary strengths.
Compared to runtime assertion checking, static verification often provides
stronger guarantees and it can give them earlier.
% at an earlier stage in the software development life cycle. 
However, these advantages come at a price:
%
SV tools generally require fairly complete specifications not only for the
module being checked, but also for the modules and libraries that it depends
on. Furthermore, in order to be effective and keep false positives to a
minimum, SV tools require specifications to make use of some of the advanced
features described in this paper.

\subsection{Outline}

The remainder of the paper is organized as follows.
The basic notation used in JML for method contracts
and invariants is covered in \secref{Sec:basics}.
\secref{Sec:assignable} explains frame properties, and \secref{Sec:model} model fields.
The treatment of behavioral subtyping is given in \secref{Sec:behsubtyping}.
\secref{Sec:ghost} explains ghost fields.
\secref{Sec:ownership} introduces the JML notations that deal with
ownership and aliasing.  
Finally, conclusions and related work are given in \secref{Sec:conclusion}.

\section{JML Basics: Pre- and Postconditions, and Invariants}
\label{Sec:basics}

%% \MARGIN{Erik: Explain \texttt{non\_null}, giving forward ref to
%% \figref{Example:alarmclock} where it is used. PC: this has not been done yet.
%% Maybe it can merely be mentioned with the alarm clock example?}
%
% Intro: Clock examples.
%
This section examines the specification and implementation of
various kinds of clocks.  In doing so, we review basic concepts such as
method contracts and class invariants and introduce their JML notation.

\subsection{Method contracts}

% intro: requires, ensures.
%
We begin with the specification of a \texttt{TickTockClock} as given in
\figref{Example:TickTockClock}.
\begin{figure}[tbp]
%
\VerbatimInput[numbers=left]{TickTockClock.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{JML specification for \texttt{TickTockClock}.
  The datagroup \texttt{\_time\_state}, the
  associated \texttt{assignable} clauses and \texttt{in} clauses are
  explained later, in Section~\ref{Sec:assignable}.} 
\label{Example:TickTockClock}
\end{figure}
This specification illustrates basic
method contracts formed by:
%
\begin{itemize}
  \item preconditions (introduced by the \texttt{requires} keyword), and
  \item postconditions (\texttt{ensures}).
\end{itemize}
An example of such a contract is found in the specification of the
method \texttt{getSecond()} on lines 23--24.  The JML specification for
each method is written in front of the method itself, and is found in
stylized Java comments 
% special annotations, which look like Java comments 
that begin with an at-sign (`\texttt{@}').

% NOTE: this doesn't seem to be quite the right time to introduce the notion
% of non-null types because, in fact, the given clock spec doesn't make use of
% reference types :). --PC
%
%% Ignoring some details for the moment,\footnote{
%% E.g., that declarations of reference types are non-null by default in JML.
%% % The omitted details are that JML, by default, asserts that formal
%% % parameters and the result of a method are not null.
%% }

% Implicit pre- and post-conditions.
% 
\GMARGIN{implicit clauses}
%
A method contract without an explicit \texttt{requires} clause has
an implicit precondition of $true$.  Thus, such a
method imposes no requirements on its callers.  This default means
that the \texttt{requires} clause written for \texttt{getHour()} could
have been omitted entirely.
Similarly, the default postcondition 
when none is explicitly given in an \texttt{ensures} clause is also
$true$, which says that the method makes no guarantees to
its caller.
%In \figref{Example:TickTockClock}, 
The constructor (on lines 11--14)
and the method \texttt{getMinute()} (on lines 20--21) are
examples of class members with implicit \texttt{requires} clauses.

Note that assertion expressions appearing in \texttt{requires} and
\texttt{ensures} clauses are written using a Java-like syntax.
%
\GMARGIN{\old}
\GMARGIN{\result}
%
In postconditions of (non-\texttt{void}) methods, \result\ can be used to refer to the 
value being returned by the method.
The only other JML specific operator used in this clock specification is the
\old$()$ operator, which is used in an \texttt{ensures} clause of
\texttt{tick} (on lines 30--32).  The 
expression \old$(e)$ refers to the value of $e$ in the method's pre-state,
i.e., the state just before the method is executed.

% \GMARGIN{multiple clauses}
Preconditions and postconditions are often split over multiple \texttt{requires}
and \texttt{ensures} clauses, as illustrated for the postcondition of 
\texttt{getSecond()} (on lines 23--24).  Multiple \texttt{ensures}
clauses, or multiple \texttt{requires} clauses, are equivalent to
a single clause consisting of the conjunction (\texttt{\&\&}) of their
respective assertions.

Method contracts, like the contract of \texttt{tick()} on lines 27--37
of \figref{Example:TickTockClock}, are written as one or
more \emph{specification cases} combined with the keyword \texttt{also}.
Each specification case is a ``mini-contract'' in itself, having a precondition
and postcondition (either explicit or implicit) as well as other clauses
that are covered below.
Use of specification cases allows developers to structure their
specifications and to (literally) break it up into (generally) distinct cases.

The contract for \texttt{tick()},
which is somewhat contrived for illustrative purposes,
highlights to clients that its behavior 
essentially has two cases of interest.  Either 
\begin{itemize}
  \item seconds are less than 59 and the seconds are incremented by one,
    or
  \item seconds are at 59 and they will be wrapped back to 0.
\end{itemize}
%
We note in passing that the specification of \texttt{tick()} is incomplete, as
it might be during the development of the \texttt{TickTockClock} class.
Informal comments, like the one on line 37, are useful for
remembering what remains to be formalized or to avoid formalization
(e.g., if it is too costly), although they do not help in verification. 

\subsection{Purity}
\label{Sec:purity}
%
In the DBC approach, only query methods can be used in assertion expressions
because they are required to be side-effect free~\cite{Meyer97}.
% 
The corresponding concept in JML is known as method \emph{purity};
pure methods are not allowed to have side effects, and pure
constructors can only assign to the fields of the object they are initializing.
Purity is statically checked by the JML tools.
The restriction that only methods
declared as \texttt{pure} can be used in assertion expressions is also
checked statically.
E.g., since the method \texttt{getSecond()} is declared \texttt{pure}, it is
legal to make use of it in the postcondition of \texttt{tick()}.

Notice that the \texttt{TickTockClock} constructor is declared as \texttt{pure}
despite the fact 
that it assigns to the fields \texttt{hour}, \texttt{minute} and \texttt{second}.
Such instance field assignments are permitted inside the bodies of constructors
because they are benevolent side-effects---i.e., that have no observable effect
on clients.
%
On the other hand, a pure constructor would not be permitted to assign to a static
field.
%
Purity, and particularly variants in the strength (restrictiveness) of its
definition are a subject of active research---e.g., a stronger notion of purity
than that of JML has been proposed by Darvas and M\"uller
\cite{DarvasMuller05}.  On the other hand, purity is often too strong
\cite{Leavens-etal05}, and so a notion of ``observational purity''
that permits benevolent side effects (such as updates to caches) is
also under consideration~\cite{Barnett-etal04a,Naumann05}.

\subsection{Lightweight vs. heavyweight}

JML actually has two kinds of specification cases: lightweight and heavyweight.
Lightweight specification cases are useful when giving partial
specifications, and in practice are often used with ESC/Java2.  To
convey that one is intending to give a complete specification for some
precondition, one would use a heavyweight specification case.
Such heavyweight specification cases are often used with runtime
assertion checking.

The specification cases of the \texttt{tick()} method are lightweight.
%
\GMARGIN{heavyweight} 
%
An example use of heavyweight specification cases is found on the
\texttt{setTime()} method of the \texttt{SettableClock} class given in
\figref{Example:SettableClock}.
%
A heavyweight specification case is easily recognized by the use of a
``\texttt{behavior}'' keyword at the beginning of the case.
%
The contract of \texttt{setTime()} illustrates the two kinds of heavyweight
specification cases most often used.
%
\GMARGIN{\texttt{normal\_behavior}}
The first specification case uses the \texttt{normal\_behavior} keyword and it
describes the intended behavior of the method when it returns normally.
%
\GMARGIN{\texttt{exceptional\_behavior}}
%
The second specification case uses the \texttt{exceptional\_behavior} keyword and it
describes the intended behavior of the method when the method raises an exception.
%
The latter case is described at greater length in \secref{Sec:Exceptions}.
Notice that the heavyweight specification cases of \texttt{setTime()} start
with \texttt{public}.
%
\GMARGIN{visibility}
%
This means that the specification cases are visible to clients, and hence, for
example, will be included as a part of client visible documentation generated
using JmlDoc~\cite{STTT05}. It also means that these specification cases cannot
refer to \texttt{private} or \texttt{protected} fields.

\begin{figure}[tbp]
%
\VerbatimInput[numbers=left]{SettableClock.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{JML specification for \texttt{SettableClock}}
\label{Example:SettableClock}
\end{figure}
%
\GMARGIN{lightweight}
%
Contracts built from lightweight specification cases have fewer keywords and
mandatory clauses.  In particular, the visibility of a lightweight
specification case cannot be given explicitly since, by definition, its
visibility is the same as 
the visibility of the method it is attached to.
%
The method contracts in \texttt{TickTockClock} are all examples of 
lightweight method specifications.

%\subsection{Completeness of specifications}
%%
%\MARGIN{PC: Do we really want to include this?}
%%
%The reader will have noticed that the specification of \texttt{tick()} is
%incomplete, since it does not show that \texttt{tick()} should also advance
%the minute and hour at the end of a full minute and hour, respectively.  One
%could write a more elaborate postcondition that is complete, but in practice
%there may be good reasons why one may not want to write complete
%specifications; \COMMENT{e.g.\ it can be too hard, too much work, or simply not
%considered interesing}.

\subsection{Exceptions and exceptional postconditions}
\label{Sec:Exceptions}

JML distinguishes two kinds of postcondition:
\begin{itemize}
  \item normal postconditions, expressed
    by means of \texttt{ensures} clauses, that must hold when a method
    terminates normally, and
    \item exceptional postconditions, expressed by means of \texttt{signals}
      clauses, that must hold when a method terminates with an exception.
\end{itemize}
%
The exceptional specification case of \texttt{SettableClock.setTime()} is
interpreted as follows: if \texttt{hour} and \texttt{minute} are not within
their valid ranges, then the method will raise an \texttt{IllegalArgumentException} 
and the system state will be left unchanged.

Notice that in the \texttt{TickTockClock} class
there are no Java \texttt{throws} clauses.
Still, Java permits the constructor and any of the methods of this class to throw a 
\texttt{Runtime\-Exception}---one commonly raised runtime exception is 
\texttt{Null\-Pointer\-Exception}.
%
JML is more strict when it comes to declaring runtime exceptions: 
whereas Java allows any constructor or method to throw a runtime exception, JML only 
allows this if the exception is listed in the method's throws clause,
or in the method contract's \texttt{signals\_only} clause.
\texttt{SettableClock.setTime()} illustrates use of the latter.
%
Therefore, constructors or methods without an explicit throws clause
have an implicit exceptional postcondition of \texttt{signals (Exception) false}.
%
So the specification in \figref{Example:TickTockClock} 
rules out the generation of any runtime exceptions, making the
specification much stronger than it might appear at first sight.
However, JML, like Java, makes a distinction between exceptions and errors; since
Java's type \texttt{Error} is not a subtype of \texttt{Exception},
JML specifications do not say anything about virtual machine errors,
such as running out of memory~\cite{Poetzsch-Heffter97}.

\subsection{Instance and static invariants (and the callback problem)}

A JML \texttt{invariant} clause declared with a
\texttt{static} modifier is called a \emph{static invariant}.
%
Static invariants express properties which must hold of the static
attributes of a class.
%
An assertion that appears in a non-static \texttt{invariant} clause is called
a \emph{instance invariant} or an \emph{object invariant}.
%
Note that while this terminology is contrary to the literature, it is more
accurate with respect to the nomenclature of Java.  In this paper, an
unqualified use of the term ``invariant'' will refer to an ``object
invariant.''

The semantics of object invariants is more involved than most specifiers
expect, especially for newcomers to the field of object-oriented specification.
Hence, while this issue has been widely known for quite some time
\cite{Szyperski98}, we believe it is worth a brief explanation.
%
Intuitively, an object invariant:
\begin{itemize}
  \item  has to be established by constructors---i.e., it is implicitly
    included in the postcondition of constructors;
  \item can be assumed to hold on entry to methods, but methods must also
    re-establish it on exit. Hence, the invariant is implicitly included in the
    preconditions, and (normal and exceptional) postconditions of methods.
\end{itemize}

This intuition may suggest that the notion of object invariant is not really
necessary, but rather that it just provides a convenient shorthand.
This idea is a
common misconception, as there is more to the notion of invariant than
the intuitions summarized above. 
One difference is that invariants apply to all subtypes through
specification inheritance (\secref{Sec:behsubtyping}), whereas
predicates that just happen to appear in all pre-and post conditions
are not inherited as part of the specification of any new methods that
may be added in a subtype.

One other issue is related to callbacks.
For example, suppose that the \texttt{tick} method called another method
at a program point where its invariant is broken, such as the call to
\texttt{canvas.paint()} in the following:
\begin{verbatim}
  public void tick() {
    second++;
    // object invariant might no longer hold
    canvas.paint();
    /* ... */
  }
\end{verbatim}
%    if (second == 60) { second = 0; minute++; }
%    if (minute == 60) { minute = 0; hour++; }
%    if (hour == 24)   { hour = 0; }
%
It would then be reasonable for the canvas to invoke, e.g., the
\texttt{getSecond()} method of the current clock object, performing a so-called 
callback. \GMARGIN{callback}
% Unfortunately, the canvas is not permitted to do so ...
However, since the invariant of this clock object is broken, its behavior is
unconstrained, in particular because the preconditions of all methods (which
implicitly include the object invariant) are all false.

To avoid such problems, the invariant not only has to be re-established at the
end of each method, but also at those program points where a
(non-helper) method is invoked.
These program points---i.e., all program points
at which a method invocation starts or ends---are called the \emph{visible
states}. The visible state semantics for invariants says that all invariants
of all objects must hold at these visible states.
\MARGIN{Do we have a reference to give here? --PC}
%
This semantics is very strong and in many cases
overly restrictive.  Less restrictive, but still sound, approaches are still a
hot topic of ongoing research. A more thorough discussion of this problem
and a proposed solution for JML is given in 
\cite{Mueller-Poetzsch-Heffter-Leavens05}; alternative solutions are
explored elsewhere
\cite{BoogieInvariants,Huizing-Kuiper00,JacobsLeinoPiessensSchulte05,Middelkoop05}.

\section{Frame properties}
\label{Sec:assignable}

In traditional specifications that give pre- and postcondition for methods
(or procedures) one often uses the convention that any variables not mentioned 
in the postcondition have not been changed.  This approach is 
\emph{not} workable for realistic object-oriented programs.
For example, consider the method \texttt{tick()} in 
\figref{Example:TickTockClock}. This method may modify the three private 
fields \texttt{second}, \texttt{minute} and \texttt{hour}, but these do 
not appear in the postcondition. Rewriting the specification so it does 
mention these fields is clearly not what we would want, since in the 
specification of this public method we do not want to refer to private fields.

A JML \texttt{assignable} clause is used in a method contract to specify
which parts of the system state \emph{may} change as the result of the
method execution.  This is the so-called \emph{frame property}
\cite{Borgida-Mylopoulos-Reiter95}.
%
Any location outside the frame property is guaranteed to have the
same value after the method has executed (called the post-state) as it did
before the method executed (in the pre-state).
%
The notion of \emph{datagroup}~\cite{Leino98} allows us to abstract
away from private implementation  
details in frame properties and provides flexibility in specifications.
% that we want to have in an object-oriented language.
This section explains these notions and the need for them.

An \texttt{assignable} clause specifies that a method may change certain 
fields without having to specify how they might change.
So the specification of the method \texttt{tick()} could include
\begin{verbatim}
   assignable hour, minute, second;
\end{verbatim}
to state that it may modify these three fields, without having to mention
the fields in the postcondition.
%
If no \texttt{assignable} clause is given for a non-pure method, then it has the
default frame condition \texttt{assignable \everything}.
However, pure methods (\secref{Sec:purity}) have a default frame of
\texttt{assignable \nothing}.

Object-oriented languages such as Java require some means for abstraction in
assignable clauses.  E.g., the first \texttt{assignable} clause for \texttt{tick()} given
above leaves a lot to be desired.  Firstly, it exposes implementation
details, because it mentions the names of protected fields.  Secondly, the
specification is overly restrictive for any future subclasses.  By the
principle of \emph{behavioral subtyping}, discussed in more detail in
\secref{Sec:behsubtyping}, the implementation of \texttt{tick()} in any
future subclass of \texttt{TickTockClock} has to meet the specification given
in \texttt{TickTockClock}.  This means that the method body can only assign to the three
fields of \texttt{TickTockClock}, which is far too restrictive in practice.  
%
To give a concrete example, suppose we introduce a subclass
\texttt{Tick\-Tock\-Clock\-With\-Date} of \texttt{TickTockClock} that, in
addition to keeping the time, also keeps track of the current date.  Clearly
such a subclass will introduce additional fields to record the date and
\texttt{tick} will have to modify these fields when the end of a day is
reached; however, the assignable clause given above will not allow these
fields to be changed, as they are not explicitly listed.

Datagroups~\cite{Leino98} provide a solution to 
this problem. The idea is that a datagroup is an abstract piece of an object's
state that may still be extended by future subclasses.
The specification in \figref{Example:TickTockClock} declares a (public) datagroup
\texttt{\_time\_state} and declares that the three (private) fields belong
to this datagroup. This datagroup is (partially) used to specify \texttt{tick()}.
This avoids exposing any private implementation details, and
subclasses of \texttt{TickTockClock} may extend the datagroup with
additional fields it introduces.

Datagroups may be nested by using the \texttt{in} clause to say that
one datagroup is part of another one. The JML specification for
\texttt{java.lang.Object} declares a datagroup named
\texttt{objectState}. Since this datagroup 
is inherited by all other classes, as a convention one can use 
\texttt{objectState}
in any class to describe what constitutes the `state' of an object of that class.
Had we followed this convention then, e.g., we would have declared the 
\texttt{\_time\_state} datagroup to be in \texttt{objectState}. 

Finally we note that, although \texttt{assignable} clauses are needed
when doing program verification, they are \emph{not} currently used during
runtime assertion checking.
(The RAC tool checks \texttt{assignable} clauses
statically and does not check them at runtime.)

\newpage
\section{Model fields}
\label{Sec:model}

\begin{figure}[tbp] 
%
\VerbatimInput[numbers=left]{Clock.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{Example JML specification illustrating the use of model fields.}
\label{Example:model}
\end{figure}

\MARGIN{We can point out the danger of the model field being
subject to an integer overflow, and explain Patrice's solution
to this. --Erik  Don't think we'll have time to add that. --P}

Model fields~\cite{Cheon-etal05} are closely related to the notion of
data abstraction proposed by 
Hoare~\cite{Hoare72}.  A model field is a specification-only field
that provides an abstraction of (part of) the concrete state of an object.  
%
The specification in \figref{Example:model} illustrates the use of a model field.
It abstracts away from the particular concrete representation of time
by using a model field \texttt{\_time} that represents the number of seconds
past midnight.
%
Notice how this abstraction allows for a brief but complete specification of the method \texttt{tick()}.
%
The \texttt{represents} clause of line 3 relates the model field to its
concrete representation, 
in this case as a function of \texttt{hour}, \texttt{minute} and 
\texttt{second}. Hence, the \texttt{represents} clause defines the 
representation function of \texttt{\_time}.  (In its most general form, JML also
permits \texttt{represents} clauses that are relational
\cite{Leavens-etal06}, but we do not discuss these here.)

Note that the \texttt{\_time} model field is public, and hence visible to
clients, though its representation is not.  The \texttt{represents} clause
must be declared private, because it refers to private fields.
%
For every model field there is an associated datagroup, so that the 
model field can also be used in \texttt{assignable} clauses.
In fact, a field of type \texttt{JMLDataGroup} is a degenerate model
field that holds no information.

A difference between model fields for objects and the traditional notion of
abstract value for abstract data types is that an object can have several
model fields, providing abstractions of different aspects of the object.
For instance, the specification of \texttt{AlarmClock}
(a subclass of \texttt{Clock}, given in \figref{Example:alarmclock}) uses 
two model fields, one for the current time, which it inherits from
\texttt{Clock}, and one for the alarm time.

Model fields are especially useful in the specification of Java interfaces,
as interfaces do not contain any concrete representation we can refer
to in specifications. We can declare model fields in a Java interface, and
then every class that implements 
the interface can define its own \texttt{represents} clause relating
this abstract field to its concrete representation. 
%
% Erik: I removed the sentence below, as overriding represents clause
%       is a dubious thing to do.
% Similarly, a subclass
% of \texttt{Clock} could choose to provide a different representation
% of time and then override the \texttt{represents} clause. For example,
% the example \texttt{DigitalDisplayClock} in \figref{Example:alias}
% does this.
%
For a more extensive discussion of model fields see~\cite{Cheon-etal05}.
Cok discusses how model fields are treated in ESC/Java2~\cite{Cok05}, while
Leino and M\"{u}ller have recently worked on handling model fields in the
context of verification~\cite{LeinoMuller06}.

\section{Behavioral subtyping and specification inheritance}
\label{Sec:behsubtyping}

JML enforces \emph{behavioral subtyping}
\cite{America90,Dhara-Leavens96,Leavens-Dhara00,Leavens-Weihl95,LiskovWing94,Meyer97}:
instances of a given type $T$ must meet the specifications of each of
type $T$'s supertypes.
This ensures Liskov's ``substitution principle''~\cite{Liskov88},
i.e., it ensures that using an object of a subclass in a place where an object of 
the superclass is expected does not cause any surprises, ensuring that 
the introduction of new subclasses does not break any existing code.
This idea is also known as supertype abstraction
\cite{Leavens90,Leavens-Weihl95}.

For example, consider the class \texttt{AlarmClock} in \figref{Example:alarmclock}.
Because \texttt{AlarmClock} is a subtype of \texttt{Clock}, it 
inherits all the specifications of \texttt{Clock}, i.e., 
all invariants specified for \texttt{Clock} also apply to \texttt{AlarmClock},
and any (overriding) method in \texttt{AlarmClock} has to meet the specification
for the corresponding method in \texttt{Clock}.
For example, the overriding \texttt{AlarmClock} method \texttt{tick()}
has to meet the specification given for it in \texttt{Clock}. 
Note that any inherited methods
that are not overridden have to be re-verified, to check
that they maintain any additional invariants of the subclass.
(\cite{Ruby-Leavens00} investigates
ways to avoid some of this re-verification.)

\begin{figure}[tbp] 
%
\VerbatimInput[numbers=left]{AlarmClock.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{Example JML specification illustrating the concepts of 
specification inheritance and ghost fields.}
\label{Example:alarmclock}
\end{figure}

\begin{figure}[tbp]
%
\VerbatimInput[numbers=left]{AlarmInterface.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{Interface of the alarm used in \texttt{AlarmClock}}
\label{Example:alarminterface}
\end{figure}

When it comes to method specifications, behavioral subtyping requires
that the specification of an overriding method $m$ must refine that of its
supertypes in the sense that whenever a supertype's precondition for
$m$ is satisfied, then the supertype's postcondition for $m$ must
hold.  It follows that the preconditions of an overriding method
may only be weaker.
Furthermore, whenever an overridden method's precondition is
satisfied then the postcondition of the overriding method must
imply the postcondition of the overridden method.
%
One way to achieve this is would be to allow a subtype to give a new
specification for a method---effectively overriding the one in the
supertype---and then prove the necessary refinement relationship.
Instead, JML uses the principle of \emph{specification inheritance} 
for method specifications~\cite{Dhara-Leavens96}: all specification cases
written for an overriding method are ``conjoined''  (using
\texttt{also}) with the specification cases of the method(s) being overridden.
Specification inheritance guarantees that the overriding method obeys all the inherited
specification cases and thus that the method satisfies a
refinement of the inherited specifications.  This automatically makes
all subtypes behavioral subtypes and thus validates the principle of
supertype abstraction.

The meaning of specification cases conjoined by \texttt{also} can be a
bit subtle.  However, it is easiest to just keep in mind that all
specification cases of all inherited methods have to each be obeyed by
a method.  
If, for a given method,
the subtype and supertypes all specify the same precondition and
assignable clause, then
the conjoined specification will be equivalent to a single 
specification case whose precondition and assignable clause are the
same as in the individual specification cases, and with a
postcondition that is the conjunction of the postconditions in the
individual specification cases.
If different preconditions are given in a sub- and supertype the
meaning of the conjoined specification cases is more involved:
the precondition of the conjoined specification will effectively be the
disjunction of the preconditions from the individual specification
cases, and the postcondition of the conjoined specification will
effectively be a conjunction of implications, where each precondition
(wrapped in \texttt{\old()}) implies the corresponding postcondition.
This effective postcondition is slightly weaker than the conjunction
of the postconditions, since each 
postcondition only has to apply in case the corresponding precondition
was satisfied~\cite{Dhara-Leavens96}.

Before closing this section we point out that the \texttt{alarm} field (line
13) and \texttt{alarm} parameter (line 15) of the \texttt{AlarmClock} class
are explicitly declared to be non-null instances of \texttt{AlarmInterface}.
While this is unnecessary (since declarations of reference types are non-null
by default in JML~\cite{Leavens-etal05,Chalin-FTfJP06}), it is also harmless
and can in fact be helpful to JML newcomers. Though we will not have the need
in our examples, declarations that may be null must be annotated with the
\texttt{nullable} modifier.

% \MARGIN{An example of this?}
% \MARGIN{Or refer to the desugaring paper?}
%
% The flexibility of object-oriented programming -- notably the notion
% of late binding -- makes it more complicated to understand programs:
% at compile time it is not clear which implementation of a
% method will be executed for a given method invocation in the code.
% This also complicates program verification.
% 
% This in turn is crucial for modular verification of code,
% where we do not have to reverify exiting code when we add a new subclass.

% We want to verify code in a modular manner,  meaning that
% that the addition of some new subclass does not necessiatate
% the re-verification of all code, but just the verification
% of the new subclass.

\section{Ghost fields}
\label{Sec:ghost}

\MARGIN{Erik: Maybe the example in this section is too involved?}

Like model fields, ghost fields are specification-only fields,
so they cannot be referred to by Java code.
While a model field provides an abstraction
of the existing state, a ghost field can provide some additional state,
which may---or may not---be related to the existing state.
Unlike a model field, a ghost field can
be assigned a value. This is done by a special \texttt{set} statement
that must be given in a JML annotation.
Before we discuss the difference between model and ghost fields
in more detail, let us first look at an example of the use of a ghost field.

% {\scriptsize A more interesting example of a ghost field is 
% Typical use pattern for ghost fields: 
% recording some information in an auxiliary field that is convenient
% for specification (eg. to specify constraints on invocation
% order of methods)  or necessary for verification (eg in loops you
% sometimes need this).
% 
% Classical example familiar from Hoare logics: ghost variable needed 
% to express some loop invariant.}
% 
% \subsection{Example ghost field: a specification-only constant}
% 
% In the specification of \texttt{Clock} using the model
% field \texttt{time}, given in Figure~\ref{Example:model} it would
% be nice to introduce a constant for the value \texttt{24*60*60}.
% We could introduce a final static field \texttt{SECONDS\_PER\_DAY} for
% this value.
% However, given this constant is only needed in specifications,
% % and not in the code, we can introduce this constant as a ghost field, 
% to be precise as a final static ghost field.
% The only difference between such a final static ghost field 
% and a normal final static field is that the former can only
% be used in specifications.
% % 
% \subsection{Example ghost field: a boolean \texttt{alarmTimeSet}}
% 
% \COMMENT{Erik: I propose dropping this example, as it
% requires a more infrastructure in the AlarmClock example, eg to
% turn alarm on/off}
% % 
% Suppose that the informal specification of \texttt{AlarmClock} says that
% \texttt{enableAlarm} should only be invoked after the alarm time has
% been set using \texttt{setAlarmTime}. Note that the implementation
% does not check this or enforce this: it is the responsibility of the
% caller to ensure this\footnote{One could argue about whether this is 
% good programming practice, but we ignore this issue here.}
% Indeed, that the state of the \texttt{AlarmClock} does not
% even record if the alarm time has been set, so there is no
% way the current implementation could check or enforce it.
% 
% To express the informal requirement above in JML we will need to 
% record in the state an on \texttt{AlarmClock} whether or not 
% \texttt{AlarmClock} has been invoked.
% This can be done by extending the state of \texttt{AlarmClock}
% with an additional boolean ghost field \texttt{alarmTimeSet}, 
% as illustrated in Figure~\ref{Example:alarmclock}.
% The spec of the constructor says that \texttt{alarmTimeSet} 
% is initially false, the spec of \texttt{enableAlarm} requires 
% that \texttt{alarmTimeSet} is true, and the spec of
% \texttt{setAlarmTime} says that  this field will be set to true.
% 
% The JML runtime assertion checker and ESC/Java2 can now point out any 
% violations of the informal requirement, at runtime and compile time, 
% respectively.
% 
% \begin{figure}[tbp]
% %
% \verbatiminput{AlarmClockGhostOne.java}
% %
% \caption{\label{example}JML specification using a ghost field 
% \texttt{alarmTimeSet} to impose a restriction on the invocation 
% order of methods for client code.}
% \label{ghost}
% \end{figure}
% 
% \subsection{Example ghost field: a boolean \texttt{\_alarmRinging}}
% \MARGIN{Erik: an alternative example might be adding a boolean ghost field 
% in the \texttt{AlarmInterface}; maybe the earlier example can then be dropped?}
% 
% Our third example of the use of a ghost field is more interesting, as
% it points a possible bug in the implementation, or at least an 
% ambuity in the informal specification.
% \medskip

Suppose that we want to convince ourselves that the implementation of 
\texttt{AlarmClock} will not invoke the method \texttt{alarm.on()}
twice in a row, or the method \texttt{alarm.off()} twice in a row,
but that it will always call \texttt{alarm.on()} and \texttt{alarm.off()}
 alternately. 
(One could add JML contracts to \texttt{AlarmInterface} to specify this
requirement, but we will not consider that here.)

The state of an \texttt{AlarmClock} object does not record if the associated
\texttt{alarm} is ringing or not, nor 
%(except maybe implicitly, in that the alarm is ringing for 60 seconds after the alarm time). 
% The state of an \texttt{AlarmClock}
does it record which method it has last invoked on \texttt{alarm}.
For the purpose of understanding the behavior of the \texttt{AlarmClock}, 
and possibly capturing this understanding in additional JML annotations,
it may be useful to add an extra boolean field to the state that records if 
the associated alarm is ringing.
%
In \figref{Example:alarmclock}, we have declared 
a boolean ghost field \texttt{\_alarmRinging}.
Two assignments to this field are included in the method \texttt{tick()}.
The assignments ensure that the field is true when the alarm ringing and false
otherwise.
%
%\footnote{
A subtle issue here is that \texttt{\_alarmRinging} has to be
  included in the datagroup associated with \texttt{\_time}. This is
  because---by the principle of specification inheritance---the method
  \texttt{tick()} is only allowed to have side effects on \texttt{\_time}.
  Since \texttt{tick()} assigns to \texttt{\_alarmRinging}, the field
  has to be included in this datagroup.  
%
  (As was mentioned in \secref{Sec:assignable}, we could have instead declared
  \texttt{\_time} to be in \texttt{objectState}, and used 
  \texttt{objectState} in the assignable clause of \texttt{tick()}.  It then
  would have been more natural to declare \texttt{\_alarmRinging} to be in
  \texttt{objectState}.)
%}.

% \begin{figure}[tbp]
% %
% \verbatiminput{AlarmClockGhostTwo.java}
% %
% \caption{\label{example}Example JML specification using ghost field \texttt{\_alarmRinging} to record if alarm is ringing}
% \label{ghosttwo}
% \end{figure}

One can now try to capture the informal requirement that 
% ``if an alarm time has been set, and the alarm is enabled, then 
``the alarm will ring for the minute that follows 
the specified alarm time,'' by formulating 
invariants relating the new ghost field \texttt{\_alarmRinging} to
the `real' state of the \texttt{AlarmClock}. There are many ways to express
such a relation, for instance using the following as the invariant:
%% [[[We should really put these in a file and check them!]]]
\begin{verbatim}
 _alarmRinging <==> _alarmTime <= _time && _time < alarmTime + 60;
\end{verbatim}
% invariant _alarmTime+60 <= 24*60*60 ==> 
%     ( _alarmRinging 
%       <==> _alarmTime <= _time && _time <= _alarmTime+60);
%
% invariant alarmtime+60 > 24*60*60 ==> 
%     ( _alarmRinging 
%       <==> 
%       ( (_alarmTime <= _time && _time <= 24*60*60)
%        ||
%        (0 <= _time && _time <= (_alarmTime+60) % 24*60*60) 
%     ) );
Verification by ESC/Java2 will immediately point out that these invariants
may be violated,
namely by invocations of \texttt{setTime} and  \texttt{setAlarmTime}.
This highlights a potential weakness in the implementation:
relying on the comparison of the current time and the alarm time
in the decision to turn the alarm off might result in unwanted behavior. 
The alarm could be turned on twice in a row, or turned off twice in a row.
Also, the alarm could ring for longer than 60 seconds, if one of these times 
is changed while the alarm is ringing.

\MARGIN{Erik: we could change the spec of
AlarmInterface, with a boolean model/ghost field, to forbid this. Of course,
if the alarm is aliased, we still have a problem.}

An improvement in the implementation is to count down the number of 
seconds left until the alarm is disabled and use this count as a basis for switching 
off the alarm, rather than relying on a comparison of the current time 
and the alarm time.

\begin{verbatim}
  /** The number of seconds remaining to keep ringing the alarm.
    * If zero, the alarm is silent (off). */
  //@ private invariant 0 <= alarmSecondsRemaining &&
  //@                   alarmSecondsRemaining <= 60;

  /*@ private invariant _alarmRinging
    @                   <==> alarmSecondsRemaining > 0; @*/
  private int alarmSecondsRemaining = 0; //@ in _time;
  ...

  public boolean tick() {
    super.tick();
    if (alarmSecondsRemaining > 0) {
      alarmSecondsRemaining--;
      if (alarmSecondsRemaining == 0) {
        alarm.off();
        //@ set _alarmRinging = false;
      }
    } else if (getHour() == alarmHour &
               getMinute() == alarmMinute) {
             alarm.on();
             alarmSecondsRemaining = 60 - getSecond();
             //@ set _alarmRinging = true;
    }
  }
\end{verbatim}
Now that we have a close correspondence between the
ghost field \texttt{\_alarmRinging} and the field
\texttt{alarmSecondsRemaining}, one could choose to replace
the ghost field by a model field:
\begin{verbatim}
 /*@ public model boolean _alarmRinging; in _time;
   @ private represents _alarmRinging
   @                       <- alarmSecondsRemaining > 0;
   @*/
\end{verbatim}
% However, for conceptual clarity, the ghost field is probably better.
% \MARGIN{I think the model field is clearer :) --PC}
%
Of course, one could also choose to turn the ghost field into a real field.
This would make the implementation simpler to understand.

\subsubsection*{Ghost vs.\ model fields.}

To recap, the crucial difference between a ghost and a model field 
is that a ghost field extends the state of an object, whereas
a model field is an abstraction of the existing state of an object.
A ghost field may be assigned to in annotations using the
special \texttt{set} keywords.
A model field cannot be assigned to, but changes value automatically
whenever some of the state that it depends on changes, as laid down
by the representation relation.

% [[[We should refer to Lieno and Mueller's recent paper about when
% model fields change here. Perhaps something like:...]]]
Since ghost fields are only changed by \texttt{set} statements, they
are only changed under program control.  Model fields, however,
potentially change their values whenever the concrete fields they
depend on change.  As Leino and M\"{u}ller recently noted~\cite{LeinoMuller06},
such instantaneous changes to model fields are not necessarily
sensible, because the computation of the model fields may assume that
various invariants hold.
%  A solution such as that proposed by Leino and M\"{u}ller should be adopted by JML. % [[[And we need to do that.]]]

% Note that for clients of a class there should be no difference between
% a model and a ghost field. However, this is only the case provided the 
% class is well-encapsulated, i.e. there is no way for the client
% to change the value of the model field by-passing the class's interface.
% Aliasing can be a problem here.
% 
% Typical use pattern for model fields (1): 
% introducing a model field in an interface spec, and then relating it to 
% the concrete implemenation is a class implementing this interface.
% 
% Typical use pattern for model fields (2): 
% introducing a model field in a class spec, as convenient abbreviation,
% and then relating it to the concrete implemenation.
% 
% After spotting a correspondence between the ghost field and
% the implementation, you may replace it by a model field.

\section{Aliasing}
\label{Sec:ownership}

\begin{figure}[tbp]
%
\VerbatimInput[numbers=left]{DigitalDisplayClock.java}
%
\vspace*{-3ex} % to fit this on one page
\caption{Clock implementation using an array and the universe type 
  system to ensure that references to this array are not leaked outside the
  current object.}
\label{Example:alias}
\end{figure}

\begin{figure}[tbp]
%
\VerbatimInput[numbers=left]{BrokenDigitalDisplayClock.java}
%
\vspace*{-2ex} % to fit this on one page
\caption{A subclass of \texttt{DigitalDisplayClock} which breaks encapsulation
  of the private array \texttt{time}, both by its constructor, which imports a
  potentially aliased reference, and the method \texttt{expose}, which exports
  a reference to \texttt{time}.}
\label{Example:aliasbroken}
\end{figure}

\noindent
The potential of aliasing is a major complication in program verification,
and indeed a major source of bugs in programs. 
To illustrate the issue, \figref{Example:alias} shows
\texttt{DigitalDisplayClock},
% a subclass of \texttt{Clock}, 
which uses an integer array \texttt{time} of length 6 
to represent time (line 13).  For the correct functioning of the clock it will be 
important that this array is not aliased by a field outside of the
class. If the array is aliased, code 
outside of this class could alter \texttt{time} and break the
invariants for the array~\cite{Noble-Vitek-Potter98}.
Indeed, the fact that the (private) invariants depend on the array 
\texttt{time} already suggest that the field needs to be alias-protected.

By inspecting the entire code of the class, it is easy to convince
oneself that references to this array are not leaked.
However, this does not guarantee that a subclass does not introduce
ways to leak references to \texttt{time}.
For example, the subclass \texttt{BrokenDigitalDisplayClock} in 
\figref{Example:aliasbroken} breaks the guarantee that \texttt{time}
will not be aliased.

There has been considerable work on extending programming languages
with some form of ownership (also known as confinement).
JML includes support for the universe type system
\cite{Mueller-Poetzsch-Heffter-Leavens03} as a way to specify
and enforce ownership constraints. As is illustrated in 
\figref{Example:alias} line 13, the \texttt{time} array is declared
as a \texttt{rep}-field\footnote{\texttt{rep} is short for representation.}
hence forbidding \texttt{time} from being aliased outside the object.
The typechecker incorporated in the JML compiler
will, e.g., warn that the class \texttt{BrokenDigitalDisplayClock}
in \figref{Example:aliasbroken} is not well-typed because it breaks 
the guarantee that \texttt{time} will not be aliased outside this class.
% [[[Referee 1's comment about the above sentence:
% What about passing time as an argument to a method? How 
% do you know it won't get captured? Or is this what is meant by 
% saying that ESC/Java2 does not handle universes yet?]]]
Verification with ESC/Java2 does not yet take universes into account
and this is still the subject of ongoing work.

% In modular verification of code, as ESC/Java2 does, one tries to
% verify the correctness of code irrespective of any future subclasses.
% Suppose that we are verifying
% \begin{verbatim}
% public class SomeOtherClass{
%  /*@ non_null @*/ int[] a = 
%  //@ invariant a.length > 1;
% 
%  //@ ensures a[0];
%  public void set(){ a[0] = 7;}
%
% }
% \end{verbatim}
% The spec of \texttt{set} is trivially satisfied.
% But how can we be sure that this method does not break the invariant
% of some \texttt{ClockUsingArray} object, whose \texttt{time} field
% is aliased to \texttt{a}? This would require a whole program analysis,
% taking into account all subclasses of \texttt{DigitalDisplayClock}.

%\section{Related Work}
%\label{Sec:conclusion}

% [[[It is not clear if the 
% same concepts could be ported to other OO notations. Would 
% the same ideas be suitable for C++? ]]]

% [[[There is no a related work section. Even though there are 
% multiple references throughout the paper to some related 
% projects, it would be more useful to have a separate section 
% that not only points to the related work but also clearly 
% provides the comparative analysis with the content of the 
% paper. For example, the conclusion mentions Spec# and that 
% is shares some language constructs. Does it mean that the
% concepts presented in the paper would work for Spec#? If 
% so, how?  Once again, how does it transfer to other OO 
% notations?]]]

\section{Conclusions}
\label{Sec:conclusion}

Preconditions, postconditions and invariants alone are insufficient to
accurately specify object-oriented programs.  This paper has illustrated some of
the more advanced specification constructs of the JML specification language,
notably: frame conditions, datagroups, model and
ghost fields, and support for alias control.

A language extension to C\# that is similar in purpose and scope to JML is
the Spec\# specification language~\cite{SpecSharp}.
%
Like JML, Spec\# enjoys tool support for runtime checking and static
verification, the latter being provided by the Boogie program verifier.
%
Spec\# and JML share similar basic and advanced language constructs, 
although details vary.  In particular, Spec\# provides a novel methodology to 
cope with object invariants~\cite{BoogieInvariants}.

As a final note, we point out that the question of which constructs are necessary and
sufficient for the specification of mainstream object-oriented
programs is far from settled.  Even the semantics for
some of the basic, let alone advanced, features discussed in this
paper are still the subject of active research as is clear from the
references given to very recent work.

\subsubsection*{Acknowledgments}

Thanks to David Cok of Eastman Kodak Company for his comments and feedback
on this paper.  Thanks also to Faraz Hussain for corrections.
The work of Joseph Kiniry and Erik Poll is funded in part by the Information 
Society Technologies programme of the European Commission, Future and 
Emerging Technologies under the IST-2005-015905 MOBIUS project.
The work of Gary Leavens was funded by the US National Science
Foundation under grants CCF-0428078 and CCF-0429567.
Patrice Chalin was funded in part by the Natural Sciences and Engineering Research Council of Canada under grant 261573-03.

\bibliographystyle{alpha}
\bibliography{fmco}

\end{document}
