% $Id: jml.tex,v 1.8 2003/11/18 02:44:48 davidcok Exp $
\documentclass{entcs}
%\usepackage{prentcsmacro_edited} % [[[What's this for?]]] It's for the fancy FMICS header
%\usepackage{hyperref}
\usepackage[english]{babel}
\usepackage{url}
\usepackage{verbatim}

\newif\ifpdf
\ifx\pdfoutput\undefined
   \pdffalse     % no PDFLaTeX
\else
   \pdfoutput=1  % PDFLaTeX
   \pdftrue
\fi

\ifpdf
\usepackage[pdftex,bookmarks=false,
            plainpages=false,naturalnames=true,
            colorlinks=true,pdfstartview=FitV,
            linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\else
\usepackage[dvips]{hyperref}
\fi

\selectlanguage{english}

\def\lastname{Burdy \emph{et al}}
\begin{document}
\begin{frontmatter}
\title{
       \vspace*{-2ex}
       An overview of JML tools and applications\\
             \href{http://www.jmlspecs.org}{\large \url{www.jmlspecs.org}}
       \vspace*{-3ex}
       }
\author[Gemplus]{Lilian Burdy},
\author[Iastate]{Yoonsik Cheon\thanksref{NSFISU}},
\author[Kodak]{David Cok},
\author[MIT]{Michael D. Ernst},
\author[KUN]{Joe Kiniry},
\author[Iastate]{Gary T. Leavens\thanksref{NSFISU}},
\author[MSR]{K. Rustan M. Leino},
\author[KUN]{Erik Poll\thanksref{VerifiCard}}
\address[Gemplus]{GEMPLUS Research Lab,
                  %Avenue du Pic de Bertagne,
                  %BP 100, 13881
                  G\'emenos, France }
\address[Kodak]{Eastman Kodak Company,
                R\&D Laboratories,
                %1700 Dewey Avenue, Building 65,
                Rochester, New York, USA}
                %14650-1816
\address[Iastate]{Dept. of Computer Science,
                  Iowa State University,
                  %226 Atanasoff Hall,
                  %Ames, Iowa 50011-1041, USA
                  Ames, Iowa, USA}
\address[MIT]{MIT Lab for Computer Science,
              %200 Technology Square,
              %NE43-524 Cambridge, MA 02139, USA
              Cambridge, Massachusetts, USA}
\address[KUN]{Dept. of Computer Science,
              University of Nijmegen,
              %Toernooiveld 1,
              Nijmegen, the Netherlands}
\address[MSR]{Microsoft Research,
              %One Microsoft Way,
              %Redmond, WA 98052, USA
              Redmond, WA, USA
\vspace*{-2ex}
              }
\thanks[NSFISU]{Supported in part by US NSF grants CCR-0097907
 and CCR-0113181.}
\thanks[VerifiCard]{Partially supported by EU-IST project VerifiCard
                  \href{http://www.verificard.org}{\url{www.verificard.org}}}
\maketitle
\begin{abstract}
  The Java Modeling Language (JML) can be used to specify the detailed
  design of Java classes and interfaces by adding annotations to Java
  source files.  The aim of JML is to provide a specification language
  that is easy to use for Java programmers and that is supported by a
  wide range of tools for specification type-checking, runtime
  debugging, static analysis, and verification.
  
  This paper gives an overview of the main ideas behind JML, the
  different groups collaborating to provide tools for JML, and the
  existing applications of JML\@.  Thus far, most applications have
  focused on code for programming smartcards written in the Java Card
  dialect of Java.
\end{abstract}

\begin{keyword}
formal methods,
formal specification,
Java,
runtime assertion checking,
static checking,
program verification
\end{keyword}

\end{frontmatter}

\vspace*{-2ex}
%=====================================================================
\section{Introduction}

JML~\cite{Leavens-Baker-Ruby99b,Leavens-Baker-Ruby03}, which stands
for ``Java Modeling Language'', is useful for specifying detailed
designs of Java classes and interfaces.  JML is a behavioral interface
specification language for Java; that is, it specifies the behavior
and the syntactic interface of Java code.  The syntactic interface of
Java code, a class or interface's method signatures, attribute types,
etc., is augmented with JML annotations that more precisely indicate
the correct usage of the API so that programmers can use it as
documentation.  In terms of behavior, JML can detail, for example, the
preconditions and postconditions for methods as well as class
invariants.

An important design goal is that JML be easy to understand for any
Java programmer. This is achieved by staying as close as possible to
Java syntax and semantics.  Another important design goal is that JML
{\em not} impose any particular design method on users; instead, JML
should be able to document existing Java programs designed in any
manner.

The work on JML was started by Gary Leavens and his colleagues and
students at Iowa State University, but has grown into a cooperative,
open effort.  Several groups worldwide are now building tools that
support the JML notation and are involved with the ongoing design of
JML\@.  The open, cooperative nature of the JML effort is important both
for tool developers and for potential users, and we welcome
participation by others.  For potential users, the fact that there are
several tools supporting the same notation is clearly an advantage.
For tool developers, using a common syntax and semantics can make it
much easier to get users interested. After all, one of the biggest
hurdles to using a new tool is often the lack of familiarity with the
associated specification language.

\medskip

The next section introduces the JML notation.  Section~\ref{tools}
then discusses the tools for JML in more detail.
Section~\ref{applications} discusses the applications of JML in the
domain of Java Card, the Java dialect for programming smartcards.
Section~\ref{related} discusses some related languages and tools, such
as OCL and other runtime assertion checkers, and 
Section~\ref{conclusions} concludes.

%=====================================================================
\section{The JML notation}
\label{notation}

JML blends Eiffel's design-by-contract approach~\cite{Meyer97} with
the Larch~\cite{Guttag-Horning93} tradition (and others that space
precludes mentioning).  Because JML supports quantifiers such as
\verb_\forall_ and \verb_\exists_, and because JML allows ``model''
(i.e., specification-only) fields, specifications can more easily be
made more precise and complete than those typically given in
Eiffel. JML uses Java's 
expression syntax in assertions, thus JML's notation is easier for
programmers to learn than one based on a language-independent
specification language like the Larch Shared
Language~\cite{Leavens-Baker-Ruby03,Leavens-etal03a} or
OCL~\cite{WarmerKleppe99}.

%% Note that I have used the newly specified constructor to illustrate
%% a point about ESC/Java below, so beware if you try to save space by
%% deleting it. -- Gary

\begin{figure}
{\small
\verbatiminput{Purse.java}}
\caption{\label{example}Example JML specification}
\end{figure}

Figure~\ref{example} gives an example of a JML specification that
illustrates its main features.
JML assertions are written as special comments in Java code,
either after \verb_//@_ or between \verb_/*@ ... @*/_, so that they
are ignored by Java compilers but can be used by tools that support
JML\@.
Within such comments JML extends the Java syntax with several keywords---in 
the example in Figure~\ref{example}, {\tt invariant}, {\tt requires},
{\tt assignable}, {\tt ensures}, and {\tt signals}.
It also extends Java's expression syntax with several operators---in
the example  \verb_\forall_, \verb_\old_, and \verb_\result_;
these begin with a backslash so they do not clash with existing
Java identifiers.

The central ingredients of a JML specification are preconditions
(given in {\tt requires} clauses),
postconditions (given in {\tt ensures} clauses),
and (class and interface) invariants.  These are all expressed as
boolean expressions in JML's extension to Java's expression syntax.

In addition to ``normal'' postconditions, JML also supports
``exceptional'' postconditions, specified in {\tt signals} clauses.
These can be used to specify what must be true when a method throws an
exception.  For example, the {\tt signals} clause in
Figure~\ref{example} specifies that {\tt debit} may throw a {\tt
  PurseException}, and, in that case, the balance will not change (as
specified by the use of the \verb+\old+ keyword).

The {\tt assignable} clause for the method {\tt debit} specifies a frame
condition, namely that {\tt debit} will assign to only the {\tt
  balance} field.  Such frame conditions are essential for
verification of code when using some of the tools described later.

\medskip

There are many additional features of JML that are not used in the
example in Figure~\ref{example}. We briefly discuss the most important
of these below.
\begin{itemize}
\item To allow specifications to be abstractions of implementation
  details, JML provides model variables, which play the role of
  abstract values for abstract data types \cite{Cheon-etal03}.

  For example, if instead of a class {\tt Purse}, we were specifying
  an interface {\tt PurseInterface}, we could introduce the balance as
  such a model variable.  A class implementing this interface could
  then specify how this model field is related to the class's
  particular representation of balance.
  
\item To support specifications that need mathematical concepts, such
  as sets or sequences, JML comes with an extensible Java library that
  provides these notions.  Thus, basic mathematical notions can be
  used in assertions as if they were Java objects.
  
\item A method can be used in assertions only if it is declared as
  {\tt pure}, meaning the method does not have any visible
  side-effects
%\footnote{There is still debate in the community about
%    the meaning of ``pure''. Many Java methods, for example, which
%    claim to have no side-effects, and thus should be pure, actually
%    do modify state due to caching, lazy evaluation, etc.}.
  For
  example, if there is a method {\tt getBalance()} that is declared as
  {\tt pure},
\begin{verbatim}
  /*@ pure @*/ int getBalance() { ... }
\end{verbatim}
  then this method can be used in the specification instead of the field
  {\tt balance}.
\item Finally, JML supports all the Java modifiers ({\tt private},
  {\tt protected}, and {\tt public}) for restricting visibility.  For
  example, invariants can be declared as {\tt private} invariants if
  they are only concerned with the private implementation details of a
  class and are not observable for clients.
\end{itemize}
%

%=====================================================================
\section{Tools for JML}
\label{tools}

For a specification language, just as for a programming language, a
range of tools is necessary to address the various needs of the
specification language's users such as reading, writing, and checking
JML annotations.\footnote{Most of these tools rely upon an underlying
  tool that typechecks a Java program and its JML specification.}

\smallskip

%% I commented this out because it introduces a list of 4 types of tools,
%% only the first two are about checking specifications.
%%   -Michael Ernst, 2003/5/18
% There are different kinds of tools for checking specifications:

\begin{itemize}
\item {\bf Runtime assertion checking and testing:}
\begin{itemize}
\item One way of checking the correctness of JML specifications is by
  runtime assertion checking, i.e., simply running the Java code and
  testing for violations of JML assertions.  Runtime assertion
  checking is accomplished using the JML compiler {\tt jmlc}
  (Section~\ref{jmlc}).
\item Given that one often wants to do runtime assertion checking in
  the testing phase, there is also a {\tt jmlunit} tool
  (Section~\ref{jmlunit}) which combines runtime assertion checking
  with unit testing.
\end{itemize}
\item {\bf Static checking and verification:} More ambitious than
  testing if the code satisfies the specifications at runtime, is
  verifying that the code satisfies its specification statically.
  Verifying a specification gives more assurance in the correctness of
  code as it establishes the correctness for all possible code paths,
  whereas runtime assertion checking is limited by the code paths
  exercised by the test suite being used.  Of course, correctness of a
  program with respect to a given specification is not decidable in
  general.  A verification tool must trade off the level of automation
  it offers (i.e., the amount of user interaction it requires) and the
  complexity of the properties and code that it can handle.  There are
  several tools for statically checking or verifying JML assertions
  providing different levels of automation and supporting different
  levels of expressivity in specifications.
\begin{itemize}
\item The program checker ESC/Java
  (Section~\ref{escjava})~\cite{Flanagan-Et-Al02} can automatically
  detect certain common errors in Java code and check relatively
  simple assertions.
\item The program checker JACK (Section~\ref{jack}) offers a similar
  functionality to ESC/Java, but is more ambitious in attempting real
  program verification.
\item The LOOP tool (Section~\ref{loop}) translates JML-annotated code
  to proof obligations that one can then try to prove using the
  theorem prover PVS\@.  The LOOP tool can handle more complicated
  specifications and code, but at the price of more user interaction.
\item The CHASE tool (Section~\ref{Chase}) checks some aspects of
  frame conditions.
\end{itemize}

\item {\bf Tools to help generate specifications: } In addition to
  these tools for checking specifications, there are also tools that
  help a developer write JML specifications, with the aim of reducing
  the cost of producing JML specifications.
\begin{itemize}
\item The Daikon tool (Section~\ref{daikon},~\cite{ErnstCGN2001:TSE})
  infers likely invariants by observing the runtime behavior
  of a program.
\item The Houdini tool~\cite{Flanagan-Et-Al01} uses ESC/Java to infer
  annotations for code.
\item The {\tt jmlspec} tool can produce a skeleton of a
  specification file from Java source and can compare the interfaces of
  two different files for consistency.
\end{itemize}

\item {\bf Documentation}: Finally, in spite of all the tools
  mentioned above, the most important `tool' of all is still the human
  who reads and writes JML specifications.  The {\tt jmldoc} tool
  (Section~\ref{jmldoc}) produces browsable HTML from JML
  specifications, in the style of Javadoc.  The resulting HTML is a
  convenient format for reading larger bodies of JML specifications.

\end{itemize}

\subsection{Documentation Generation}
\label{jmldoc}

Since JML specifications are meant to be read and written by ordinary
Java programmers, it is important to support the conventional ways
that these programmers create and use documentation.  Consequently,
the {\tt jmldoc} tool (authored by David Cok)
produces browsable HTML pages containing both the
API and the specifications for Java code, in the style of pages
generated by Javadoc~\cite{Friendly95}.

This tool reuses the parsing and checking performed by the JML checker
and connects it to the doclet API underlying Javadoc.  In this way,
\texttt{jmldoc} remains consistent with the definition of JML and
creates HTML pages that are very familiar to a user of Javadoc.  The
{\tt jmldoc} tool also combines and displays in one place all of the
specifications (inherited, refined, etc.)\ that pertain to a given
class, interface, method, or field.  It also combines annotations
across a series of source files that constitute successive refinements
of a given class or interface.
%% [[[KRML:  I thought the following would be a helpful example, but is
%% it true?  JRK: No, something like this isn't yet available.
%% GTL: Well, the generated HTML displays the inherited specs, as
%% described above, but the source with the documentation in it isn't
%% changed.  I think this addresses your question.]]]
% For example, it copies into the documentation of a subclass the
% inherited specifications of inherited or overridden methods.

%\section{Dynamic Techniques for JML}
%\label{dynamic}
%
%This section discusses tools that extract information from runs of
%Java code.

%\subsection{JML Tools from Iowa State University}
%\section{General Language Support Tools}
%\label{general}

%The Iowa State group provides a suite
%of JML tools including typechecker, compiler, and a unit testing tool.
%The typechecker (\texttt{jml}) is not important to most users, however,
%because its features are subsumed by other tools.

\subsection{Runtime Assertion Checking}
\label{jmlc}

The JML compiler (\texttt{jmlc}), developed at Iowa State University,
is an extension to a Java compiler and compiles Java programs
annotated with JML specifications into Java
bytecode~\cite{Cheon-Leavens02b}.  The compiled bytecode includes
runtime assertion checking instructions that check JML specifications
such as preconditions, normal and exceptional postconditions,
invariants, and history constraints.  The execution of such assertion
checks is transparent in that, unless an assertion is violated, and
except for performance measures (time and space), the behavior of the
original program is unchanged.  The transparency of runtime assertion
checking is guaranteed, as JML assertions are not allowed to have any
side-effects~\cite{Leavens-etal03a}.

The JML language provides a rich set of specification facilities to
write abstract, complete behavioral specifications of Java program
modules~\cite{Leavens-etal03a}.  It opens a new possibility in runtime
assertion checking by supporting abstract specifications written in
terms of specification-only declarations such as model fields, ghost
fields, and model methods.  Thus the JML compiler represents a
significant advance over the state of the art in runtime assertion
checking as represented by design by contract tools such as
Eiffel~\cite{Meyer97} or by Java tools such as
iContract~\cite{Kramer98} or Jass~\cite{Bartetzko-etal01}.  The
\texttt{jmlc} tool also supports advances such as (stateful) interface
specifications, multiple inheritance of specifications, various forms
of quantifiers and set comprehension notation, support for strong and
weak behavioral subtyping~\cite{Liskov-Wing94,Dhara-Leavens96}, and a
contextual interpretation of undefinedness~\cite{Leavens-etal03a}.

In sum, the JML compiler brings ``programming benefits'' to formal
interface specifications by allowing Java programmers to use JML
specifications as practical and effective tools for debugging,
testing, and design by contract.

\subsection{Unit Testing}
\label{jmlunit}

A formal specification can be viewed as a test
oracle~\cite{Peters-Parnas98,Antoy-Hamlet00}, and a runtime assertion
checker can be used as the decision procedure for the test
oracle~\cite{Cheon-Leavens02}.  This idea has been implemented as a
unit testing tool for Java (\texttt{jmlunit}), by combining JML with
the popular unit testing tool JUnit for Java~\cite{Beck-Gamma98}.  The
\texttt{jmlunit} tool, developed at Iowa State University, frees the
programmer from writing most unit test code and significantly
automates unit testing of Java classes and interfaces.

The tool generates JUnit test classes that rely on the JML runtime
assertion checker.  The test classes send messages to objects of the
Java classes under test.  The testing code catches assertion violation
errors from such method calls to decide if the test data violate the
precondition of the method under test; such assertion violation errors
do not constitute test failures.  When the method under test satisfies
its precondition, but otherwise has an assertion violation, then the
implementation failed to meet its specification, and hence the test
data detects a failure~\cite{Cheon-Leavens02}.  In other words, the
generated test code serves as a test oracle whose behavior is derived
from the specified behavior of the class being tested.  The user is
still responsible for generating test data; however the test classes
make it easy for the user to supply such test data. In addition, the
user can supply hand-written JUnit test methods if desired.

Our experience shows that the tool allows us to perform unit testing
with minimal coding effort and detects many kinds of errors.
Ironically, about half of our test failures were caused by
specification errors, which shows that the approach is also useful for
debugging specifications.  In addition, the tool can report coverage
information, identifying assertions that are always true or always
false, and thus indicating deficiencies in the set of test cases.
However, the approach requires specifications to be fairly complete
descriptions of the desired behavior, as the quality of the generated
test oracles depends on the quality of the specifications. Thus, the
approach trades the effort one might spend in writing test cases for
effort spent in writing formal specifications.

\subsection{Invariant Detection with Daikon}
\label{daikon}

Most tools that work with JML assume the existence of a JML
specification, then verify code against the specification.  Writing
the JML specification is left to a programmer.  Because this task can
be time-consuming, tedious, and error-prone, the Daikon invariant
detector~\cite{ErnstCGN2001:TSE} provides
assistance in creating a specification.  Daikon outputs observed
program properties in JML form and automatically inserts them into a
target program.

The Daikon tool dynamically detects likely program invariants.  In
other words, given program executions, it reports
properties that were true over those executions.  It operates by
observing values that a program computes at runtime, generalizing over
those values, and reporting the resulting properties.  Like any
dynamic analysis, the technique is not sound: other executions may
falsify some of the reported properties.  (Furthermore, the actual
behavior of the program is not necessarily the same as its intended
behavior.)  However, Daikon uses static analysis, statistical tests,
and other mechanisms to suppress false positives~\cite{ErnstCGN2000:Relevance}.
Even if a property
is not true in general, Daikon's output provides valuable information
about the test suite over which the program was run.

Even with modest test suites, Daikon's output is highly accurate.  In
one set of experiments~\cite{NimmerE02:ISSTA}, over 90\% of the
properties that it reported were verifiable by ESC/Java (the other
properties were true, but were beyond the capabilities of ESC/Java),
and it reported over 90\% of the properties that ESC/Java needed in
order to complete its verification.  For example, if Daikon generated
100 properties, users had only to delete less than 10 properties and
to add another 10 properties in order to have a verifiable set of
properties.  In another experiment~\cite{NimmerE02:FSE}, users who
were provided with Daikon output (even from unrealistically bad test
suites) performed statistically significantly better on a program
verification task than did users who did not have such assistance.

%\section{Static Techniques for JML}
%\label{static}
%
%More ambitious than {\em testing} if the code satisfies the specifications
%at runtime, by doing runtime assertion checking, is
%{\em verifying} that the code
%satisfies its specifications statically.
%This can give more assurance in the correctness of code:
%verification establishes the correctness for all possible inputs,
%unlike runtime assertion checking, which is always limited by the test
%suite being used.
%
%Correctness of a program with respect to
%a given specification is not decidable in general.
%A verification tool must trade off the level of automation the tool
%offers (i.e., the amount of user interaction it requires)
%and the expressiveness of the properties and code that it can handle.
%There are several tools for verification of JML assertions,
%that provide different levels of automation
%and support different levels of expressivity in specifications.

\subsection{Extended Static Checking with ESC/Java}
\label{escjava}

The ESC/Java tool~\cite{Flanagan-Et-Al02}, developed at Compaq
Research, performs what is called ``extended static checking'', static
checking that goes well beyond type checking.  It can check relatively
simple assertions and can check for certain kinds of common errors in
Java code, such as dereferencing \texttt{null} or indexing an array
outside its bounds.  The tool is fully automated, and the user
interacts with it only by supplying JML annotations in the code.
Thus, the user never sees the theorem prover that is doing the actual
work behind the scenes.

An interesting property of ESC/Java is that it is neither sound nor
complete.  This is a deliberate design choice: the aim is to maximize
the useful feedback the tool can give---i.e., the number of potential
bugs in the code it will point out---fully automatically, without
requiring full functional specifications.

In a sense, ESC/Java uses JML annotations to suppress spurious warning
messages. For example, in Figure~\ref{example},
the conjunct \texttt{p != null} in constructor's precondition causes
ESC/Java not to warn about the possibility of null dereferences on the
formal parameter \texttt{p} in the body of the constructor.
Such annotations also cause ESC/Java to perform additional checks. For
example, the precondition on the constructor of \texttt{Purse} causes
ESC/Java to emit warnings
when the actual parameter passed as \texttt{p} to the
constructor may be null.
Thus, the addition of JML annotations helps give better quality
warnings, the use of ESC/Java fosters more annotations, and in turn
these annotations help the tool do a better job of checking code for
potential errors.

ESC/Java works by translating a given JML-annotated Java program into
verification conditions~\cite{LeinoSaxeStata:JavaViaGC}, which are
then passed to an automatic theorem prover.  The ESC/Java User's
Manual~\cite{escjava:userman} provides a detailed description of the
semantics of JML annotations, as they pertain to ESC/Java.

As of this writing, there are some small syntactic and semantic
differences between JML and the subset of JML supported by ESC/Java.
Kiniry and Cok are working on patches to fix this problem.  The next
version of ESC/Java will accept all notation that has been introduced
since ESC/Java's last release, and it will ignore all non-critical
annotations it does not understand.

\subsection{CHASE}
\label{Chase}

One source of unsoundness of ESC/Java is that it does not check {\tt
  assignable} clauses.  The semantics of these frame axioms are also
not checked by the JML compiler.  The CHASE tool~\cite{CH03} tries to
remedy these problems.  It performs a syntactic check on {\tt
  assignable} clauses, which, in the spirit of ESC/Java, is neither
sound nor complete, but which spots many mistakes made in {\tt
  assignable} clauses.  This is another example of the utility of a
common language; developers can reap the benefits of complementary
tools.
%% \footnote{Current work on ESC/Java by David Cok and Joe Kiniry intends
%%   to added checking of \texttt{assignable} clauses.}

\subsection{Program Verification with LOOP}
\label{loop}

The University of Nijmegen's LOOP tool~\cite{Jacobs-etal98,Huisman01}
translates JML-annotated Java code into proof obligations for the
theorem prover PVS \cite{OwreRRSS96}.  One can then try to prove these
obligations, interactively, in PVS\@.  The translation from JML to
formal proof obligations builds on a formal semantics for sequential
Java that has has been formalized in PVS, and which has been extended
to provide a formal semantics for a large part of JML\@.  The
verification of the proof obligations is accomplished using a Hoare
Logic~\cite{JacobsPoll01a} and a weakest-precondition
calculus~\cite{Jacobs03} for Java and JML\@.  Interactive theorem
proving is very labor-intensive, but allows verification of more
complicated properties than can be handled by extended static checking
with ESC/Java.  A recent paper describing a case study with the LOOP
tool, giving the best impression of the state of the art, is now
available~\cite{BreunesseBJ02}.

A similar program verification tool for JML-annotated code under
development is the Krakatoa tool~\cite{krakatoa03a}; it produces proof
obligations for the theorem prover Coq, but currently covers only a
subset of Java.

\subsection{Static Verification with JACK}
\label{jack}

The JACK \cite{JACK} tool has been developed at the research lab
of Gemplus, a manufacturer of smartcards and smartcard software.  JACK
aims to provide an environment for Java and Java Card program
verification using JML annotations.  It implements a fully automated
weakest precondition calculus in order to generate proof obligations
from JML-annotated Java sources. Those proof obligations can then be
discharged using a theorem prover.  Currently the proof obligations
are generated for the B~\cite{Abrial96} method's prover.

The approach taken in JACK is somewhere between those of ESC/Java and
LOOP, but probably closer to LOOP than to ESC/Java, trying to get the
best of both worlds.  On the one hand, JACK is much more ambitious
than ESC/Java, in that it aims at real program verification rather
than just extended static checking, and JACK does not make all the
assumptions that result in soundness issues in ESC/Java, some of which
were made to speed up checking.  On the other hand, JACK does not
require its users to have expertise in the use of a theorem prover as
LOOP does.

An important design goal of the JACK tool is to be usable by normal
Java developers, allowing them to validate their own code.  Thus, care has
been taken to hide the mathematical complexity of the
underlying concepts, and JACK provides a dedicated proof obligation
viewer. This viewer presents the proof obligations as execution paths
within the program, highlighting the source code relevant to the proof
obligations. Moreover, goals and hypotheses are displayed in a
Java/JML-like notation.  To allow developers to work in a familiar
environment, JACK is integrated as a plug-in in the
%% [[[KRML: Is there an appropriate~\cite for Eclipse, perhaps one
%% mentioning this URL?  JRK: I think it isn't even necessary, as
%% Eclipse is a widely known, non-academic IDE\@.  Also, we didn't/won't
%% include a cite for jContract either.]]]
Eclipse\footnote{\url{http://www.eclipse.org}} IDE\@.

As earlier mentioned, JACK provides an interface to the automatic
theorem prover of the Atelier B toolkit. The prover can usually
automatically prove up to 90\% of the proof obligations; the remaining
ones have to be proved outside of JACK, using the classical B proof
tool.  However, JACK is meant to be used by Java developers, who
cannot be expected to use the B proof tool.  Therefore, in addition to
the proved and unproved states, JACK adds a ``checked'' state, that
allows developers to indicate that they have manually checked the
proof obligation. In order to better handle those cases, other different
approaches could be investigated, such as integration with test
tools such as {\tt jmlunit}, integration of other proof assistants, or
at least support from a proof-expert team.

Despite using formal techniques, the goal of JACK is not only to allow
formal methods experts to prove Java applet correctness, but also to
allow Java programmers to obtain high assurance of code correctness.
This may be a way to let non-experts venture into the formal world.

%=====================================================================
\section{Applications of JML to Java Card}
\label{applications}

Although JML is able to specify programs written in the full Java language,
most of the serious applications of JML and JML tools up to now
have targeted Java Card.  Java Card$^{TM}$ is a dialect of Java specifically
designed for the programming of the latest generation of smartcards.
Java Card is adapted to the hardware limitations of smartcards; for
instance, it does not support floating point numbers, strings, object
cloning, or threads.

Java Card is a well-suited target for the application of formal
methods.  It is a relatively simple language with a restricted API\@.
Moreover, Java Card programs, called ``applets'', are small, typically
on the order of several KBytes of bytecode.  Additionally, correctness
of Java Card programs is of crucial importance, since they are used in
sensitive applications such as bank cards and mobile phone SIMs.  (An
interesting overview of security properties that are relevant for Java
Card applications is available~\cite{MarletLM01}.)

JML, and several tools for JML, have been used for Java Card,
especially in the context of the EU-supported project VerifiCard
(www.verificard.org).  JML has been used to write a formal
specification of almost the entire Java Card
API~\cite{PollBergJacobs01}.  This experience has shown that JML is
expressive enough to specify a non-trivial existing API\@.  The
runtime assertion checker has been used to specify and verify a
component of a smartcard operating system~\cite{PollHarteldeJong02}.

ESC/Java has been used with great success to verify a realistic
example of an electronic purse implementation in Java
Card~\cite{CatanoHuisman02}. This case study was instrumental in
convincing industrial users of the usefulness of JML and feasibility
of automated program checking by ESC/Java for Java Card applets.  This
provided the motivation for the development of the JACK tool discussed
earlier, which is specifically designed for Java Card programs.  One
of the classes of the electronic purse mentioned above has provided
the most serious case study to date with the LOOP
tool~\cite{BreunesseBJ02}.

%=====================================================================
\section{Related Work}
\label{related}

\subsection{Other runtime assertion checkers}

Many runtime assertion checkers for Java exist, for example, Jass,
iContract, and Parasoft's jContract, to name just a few.  Each of
these tools has its own specification language, thus specifications
written for one tool do not work in any other tool.  And while some of
these tools support higher-level constructs such as quantifiers, all
are quite primitive when compared to JML\@.  For example, none include
support for purity specification and checking, model methods,
refinements, or unit test integration.  The developers of Jass have
expressed interest in moving to JML as their specification language.

%% We explained in Section~\ref{jmlc} why we believe that the JML
%% provides a significant advance in expressivity versus such design by
%% contract tools.

\subsection{JML vs.\ OCL}

Despite the similarity in the acronyms, JML is {\em very} different in
its aims from UML~\cite{RumbaughJacobsonBooch98}.  Unlike UML, which
attempts to have notations for all phases of the analysis and design
process, JML has the much more modest aim of describing the behavior
of Java classes and interfaces and recording detailed design and
implementation decisions.

JML does have some things in common with the Object Constraint
Language (OCL), which is part of the UML standard.  Like JML, OCL can
be used to specify invariants and pre- and postconditions.  An
important difference is that JML explicitly targets Java, whereas OCL
is not specific to any one programming language.  One could say that
JML is related to Java in the same way that OCL is related to UML\@.

JML clearly has the disadvantage that it can not be used for, say, C++
programs, whereas OCL can.  But it also has obvious advantages when it
comes to syntax, semantics, and expressivity.  Because JML sticks to
the Java syntax and typing rules, a typical Java programmer will
prefer JML notation over OCL notation, and, for instance, prefer to
write (in JML):
\begin{verbatim}
     invariant pin != null && pin.length == 5;
\end{verbatim}
rather than the OCL:
\begin{verbatim}
    inv: pin <> null and pin->size() = 5
\end{verbatim}
JML supports all the Java modifiers such as {\tt static}, {\tt
  private}, {\tt public}, etc., and these can be used to record
detailed design decisions.  Furthermore, there are legal Java
expressions that can be used in JML specifications but that cannot be
expressed in OCL\@.
% Thus JML can specify more details about Java programs than would be
% possible in OCL\@.

More significant than these limitations, or differences in syntax, are
differences in semantics.  JML builds on the (well-defined) semantics
of Java. So, for instance, {\tt equals} has the same meaning in JML
and Java, as does {\tt ==}, and the same rules for overriding,
overloading, and hiding apply.  One cannot expect this for OCL\@.  In
fact, a semantics for OCL was only recently
proposed~\cite{brucker.ea:proposal:2002}.

In all, we believe that a language like JML, which is tailored to
Java, is better suited for recording the detailed design of a Java
programs than a generic language like OCL\@.  Even if one uses UML in
the development of a Java application, it may be better to use JML
rather than OCL for the specification of object constraints,
especially in the later stages of the development.

%=====================================================================
\section{Conclusions}
\label{conclusions}

We believe that JML presents a promising opportunity to introduce
formal specification to industry.  It has the following strong points:

\begin{enumerate}
\item JML is {\em easy to learn} for any Java programmer, since its
  syntax and semantics are very close to Java.
  
  We believe this a crucial advantage, as the biggest hurdle to
  introducing formal methods in industry is often that people are not
  willing, or do not have the time, to learn yet another language.
  
\item There is no need to invest in the construction of a formal model
  before one can use JML\@. Or rather: the source code {\em is} the
  formal model.  This brings two further advantages:
  \begin{itemize}
  \item It is easy to introduce the use of JML {\em gradually}, simply
    by adding the odd assertion to some Java code.
  \item JML can be used {\em for existing} (legacy) code and APIs.
    Indeed, most applications of JML and its tools to date
    (e.g.,~\cite{BreunesseBJ02,CatanoHuisman02,PollBergJacobs01}) have
    involved existing APIs and code.
  \end{itemize}

\item There is a (growing) availability of a wide range of tool
      support for JML\@.
\end{enumerate}

Unlike B, JML does not impose a particular design method on its users.
Unlike UML, VDM, and Z, JML is tailored to specifying both the syntactic
interface of Java code and its behavior.
Therefore, JML is better suited than these alternative languages
for documenting the detailed design of existing Java programs.

\smallskip

As a common notation shared by many tools, JML offers users multiple
tools supporting the same notation.  This frees them from having to
learn a whole new language before they can start using a new tool.
The shared notation also helps the economics both for users and tool
builders.  Any industrial use of formal methods will have to be
economically justified, by comparing the costs (the extra time and
effort spent) against the benefits (improvements in quality, number of
bugs found).  Having a range of tools, offering different levels of
assurance at different costs, makes it much easier to start using JML\@.
One can begin with a technique that requires the least time and effort
(perhaps runtime assertion checking) and then move to more
labor-intensive techniques if and when that seems worthwhile, until
one has reached a combination of tools and techniques that is
cost-effective for a particular situation.

%% [[[From reviewer #1: The JML effort comprises tools that have been
%% specifically developed for it ( jml, jmlunit, jmldoc,...) and
%% previously existing tools that have been adapted to JML (daikon,
%% ESC/Java,...). It should be clear that for this project to work, it is
%% important to achieve a seamless integration of these tools. It may be
%% a good idea to add a few comments on the problems the authors have
%% faced to integrate these tools, and the degree of integration they
%% have achieved so far.]]]

\smallskip

There are still many opportunities for further development of both the
JML language and its tools.  For instance, we would also like to see
support for JML in IDEs and integration with other kinds of static
checkers.  We believe that, as a common language, JML can provide an
important vehicle to transfer more tools and techniques from academia
to industry.

More generally, there are still many open issues involving the
specification of object-oriented systems.  When exactly should
invariants hold?  How should concurrency properties be specified?
JML's specification inheritance forces subtypes to be behavioral
subtypes \cite{Dhara-Leavens96,Leavens-Baker-Ruby03}, but subtyping in
Java is used for implementation inheritance as well; is it practical
to always weaken the specifications of supertypes enough so that their
subtypes are behavioral subtypes?
There are also semantics issues with frame axioms, pure
methods, and aliasing.  Such subtleties are evidenced by the slightly
different ways in which different tools approach these problems.

%% [[[JRK: add refs for these issues or not?
%% EP Let's not: we seem to have plenty of references already.]]]

\smallskip

As witnessed by the development of the JACK tool by Gemplus, Java Card
smartcard programs may be one of the niche markets where formal
methods have a promising future. Here, the cost that companies are
willing to pay to ensure the absence of certain kinds of bugs is quite
high.  It seems that, given the current state of the art, using static
checking techniques to ensure relatively simple properties (e.g., that
no runtime exception ever reaches the top-level without being caught)
seems to provide an acceptable return-on-investment.  It should be
noted that the very simplicity of Java Card is not without its
drawbacks.  In particular, the details of its very primitive
communication with smartcards (via a byte array buffer) is not easily
abstracted away from.  It will be interesting to investigate if J2ME (Java 2
Micro Edition), which targets a wider range of electronic consumer
products, such as mobile phones and PDAs, is also an interesting
application domain for JML\@.

\subsection*{Acknowledgments}

Despite the long list of authors, still more people have been involved
in developing the tools discussed in this paper, including
Joachim van den Berg,
Cees-Bart Breunesse,
N\'estor Cata{\~n}o,
Cormac Flanagan,
Mark Lillibridge,
Marieke Huisman,
Bart Jacobs,
Jean-Louis Lanet,
Todd Millstein,
Greg Nelson,
Jeremy Nimmer,
Antoine Requet,
Clyde Ruby,
and James B. Saxe.
Thanks to Raymie Stata for his initiative in getting the JML and
ESC/Java projects to agree on a common syntax.  Work on the JML tools
at Iowa State builds on the MultiJava compiler written by Curtis
Clifton as an adaptation of the Kopi Java compiler.

\small
\bibliographystyle{plain}
\bibliography{jml}

\end{document}
