The Java Modeling Language (JML) is a
specification language
A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executa ...
for
Java
Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mo ...
programs, using
Hoare style pre- and
postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
s and
invariants, that follows the
design by contract paradigm. Specifications are written as
Java annotation
In the Java computer programming language, an annotation is a form of syntactic metadata that can be added to Java source code. Classes, methods, variables, parameters and Java packages may be annotated. Like Javadoc tags, Java annotations ...
comments to the source files, which hence can be compiled with any Java
compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
.
Various verification tools, such as a runtime assertion checker and the Extended Static Checker (
ESC/Java
ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as exten ...
) aid development.
Overview
JML is a behavioural interface specification language for Java modules. JML provides
semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and compu ...
to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from
Eiffel
Eiffel may refer to:
Places
* Eiffel Peak, a summit in Alberta, Canada
* Champ de Mars – Tour Eiffel station, Paris, France; a transit station
Structures
* Eiffel Tower, in Paris, France, designed by Gustave Eiffel
* Eiffel Bridge, Ungheni, ...
,
Larch
Larches are deciduous conifers in the genus ''Larix'', of the family Pinaceae (subfamily Laricoideae). Growing from tall, they are native to much of the cooler temperate northern hemisphere, on lowlands in the north and high on mountains furt ...
and the
Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.
Syntax
JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form
//@
or
/*@ @*/
Basic JML syntax provides the following keywords
; requires
: Defines a precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
If a precondition is violated, the effect of th ...
on the method
Method ( grc, μέθοδος, methodos) literally means a pursuit of knowledge, investigation, mode of prosecuting such inquiry, or system. In recent centuries it more often means a prescribed process for completing a task. It may refer to:
*Scien ...
that follows.
; ensures
: Defines a postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
on the method that follows.
; signals
: Defines a postcondition for when a given Exception is thrown by the method that follows.
; signals_only
: Defines what exceptions may be thrown when the given precondition holds.
; assignable
: Defines which fields are allowed to be assigned to by the method that follows.
; pure
: Declares a method to be side effect free (like assignable \nothing
but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.
; invariant
: Defines an invariant property of the class.
; loop_invariant
: Defines a loop invariant
In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in ...
for a loop.
; also
: Combines specification cases and can also declare that a method is inheriting specifications from its supertypes.
; assert
: Defines a JML assertion.
; spec_public
: Declares a protected or private variable public for specification purposes.
Basic JML also provides the following expressions
; \result
: An identifier for the return value of the method that follows.
; \old()
: A modifier to refer to the value of the
at the time of entry into a method.
; (\forall ; ; )
: The universal quantifier
In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...
.
; (\exists ; ; )
: The existential quantifier
In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
.
; a > b
: a
implies b
; a < b
: a
is implied by b
; a <> b
: a
if and only if b
as well as standard Java syntax
The syntax of Java refers to the set of rules defining how a Java program is written and interpreted.
The syntax is mostly derived from C and C++. Unlike in C++, in Java there are no global functions or variables, but there are data member ...
for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like
public class BankingExample
{
public static final int MAX_BALANCE = 1000;
private /*@ spec_public @*/ int balance;
private /*@ spec_public @*/ boolean isLocked = false;
//@ public invariant balance >= 0 && balance <= MAX_BALANCE;
//@ assignable balance;
//@ ensures balance 0;
public BankingExample()
{
this.balance = 0;
}
//@ requires 0 < amount && amount + balance < MAX_BALANCE;
//@ assignable balance;
//@ ensures balance \old(balance) + amount;
public void credit(final int amount)
{
this.balance += amount;
}
//@ requires 0 < amount && amount <= balance;
//@ assignable balance;
//@ ensures balance \old(balance) - amount;
public void debit(final int amount)
{
this.balance -= amount;
}
//@ ensures isLocked true;
public void lockAccount()
{
this.isLocked = true;
}
//@ requires !isLocked;
//@ ensures \result balance;
//@ also
//@ requires isLocked;
//@ signals_only BankingException;
public /*@ pure @*/ int getBalance() throws BankingException
{
if (!this.isLocked)
{
return this.balance;
}
else
{
throw new BankingException();
}
}
}
Full documentation of JML syntax is availabl
in the JML Reference Manual
Tool support
A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
jmlc
which converts JML annotations into runtime assertions, a documentation generator jmldoc
which produces Javadoc
Javadoc (originally cased JavaDoc) is a documentation generator created by Sun Microsystems for the Java language (now owned by Oracle Corporation) for generating API documentation in HTML format from Java source code. The HTML format is used ...
documentation augmented with extra information from JML annotations, and a unit test generator jmlunit
which generates JUnit
JUnit is a unit testing framework for the Java programming language. JUnit has been important in the development of test-driven development, and is one of a family of unit testing frameworks which is collectively known as xUnit that originated ...
test code from JML annotations.
Independent groups are working on tools that make use of JML annotations. These include:
* ESC/Java2br>
an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.
OpenJML
declares itself the successor of ESC/Java2.
Daikon
a dynamic invariant generator.
* KeY
Key or The Key may refer to:
Common meanings
* Key (cryptography), a piece of information that controls the operation of a cryptography algorithm
* Key (lock), device used to control access to places or facilities restricted by a lock
* Key (ma ...
, which provides an open source theorem prover with a JML front-end and an Eclipse
An eclipse is an astronomical event that occurs when an astronomical object or spacecraft is temporarily obscured, by passing into the shadow of another body or by having another body pass between it and the viewer. This alignment of three ce ...
plug-in
JML Editing
with support for syntax highlighting
Syntax highlighting is a feature of text editors that are used for programming, scripting, or markup languages, such as HTML. The feature displays text, especially source code, in different colours and fonts according to the category of terms. ...
of JML.
Krakatoa
a static verification tool based on th
Why
verification platform and using the Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proo ...
proof assistant.
JMLEclipse
a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
Sireum/Kiasan
a symbolic execution based static analyzer which supports JML as a contract language.
a tool to generate files for running JUnit tests on JML annotated Java files.
TACO
an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
References
* Gary T. Leavens
Gary T. Leavens is an American academic working as a professor of computer science at the University of Central Florida.
Education
Leavens earned a Bachelor of Science in computer and communication science from the University of Michigan, a Mas ...
and Yoonsik Cheon. ''Design by Contract with JML''; Draft tutorial.
* Gary T. Leavens
Gary T. Leavens is an American academic working as a professor of computer science at the University of Central Florida.
Education
Leavens earned a Bachelor of Science in computer and communication science from the University of Michigan, a Mas ...
, Albert L. Baker, and Clyde Ruby. ''JML: A Notation for Detailed Design''; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), ''Behavioral Specifications of Businesses and Systems'', Kluwer, 1999, chapter 12, pages 175-188.
* Gary T. Leavens
Gary T. Leavens is an American academic working as a professor of computer science at the University of Central Florida.
Education
Leavens earned a Bachelor of Science in computer and communication science from the University of Michigan, a Mas ...
, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009
HTML
* Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. ''Formal specification with JML''. 2014
download (CC-BY-NC-ND)
External links
JML website
Java platform
Formal specification languages
Articles with example Java code