An overview of JML tools and applications

By Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll. International Journal on Software Tools for Technology Transfer (STTT), 2003

944 citations recorded by the source corpus.

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 typechecking, runtime debugging, static analysis, and verification.This paper gives an overview of the main ideas behind JML, details about JML’s wide range of tools, and a glimpse into existing applications of JML.

Subfields: Artificial Intelligence, Software

View Paper: https://www.semanticscholar.org/paper/0035550a81b03420debb9b7962eee5ecdaa2260e

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Software

Citations in the corpus

The Spec# Programming System: An Overview (2004, methodology): “An impressive array of tools have been build around JML, including tools for documentation, run-time checking, unit testing, light-weight contract checking, and program verification [12].”
Why3: Shepherd Your Herd of Provers (2011, background): “We intend to promote these constructions to existing speciﬁcation languages, such as ACSL [4] or JML [10].”
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (2007, methodology): “For Java (and Java Card), these speci cations are given in the Java Modeling Language [1] and are interpreted by the Krakatoa tool.”
Verification of Object-Oriented Programs with Invariants (2003, methodology): “Another tool in the JML family [ 7 ] is the Extended Static Checker for Java (ESC/Java) [16], which checks JML specifications statically.”
Building a push-button RESOLVE verifier: Progress and challenges (2011, neutral): “Aside from ESC/Java2, there are a number of different verification efforts underway that also use JML to specify Java code [ 7 ].”
A Software Analysis Perspective (2012, methodology): “ACSL is a formal specification language inspired by Java’s JML [9], both being based on the notion of function contract introduced by Eiffel [42].”
The Daikon system for dynamic detection of likely invariants (2007, methodology): “Java Modeling Language [6] format, used by many tools [7].”
Hybrid type checking (2006, methodology): “JML specifications [ 8 , 26] using the Simplify automatic theorem prover [12].”
Aspect-oriented programming and modular reasoning (2005, background): “These include higher-order value typing like generic types, [5] state typing [10], behavioral specification [6, 27, 30] and others.”
Verifiable functional purity in java (2008, background): “Spec# [4] and JML [7, 13] are extensions to C# and Java that allow the programmer to specify invariants on functions and classes.”
ABS: A Core Language for Abstract Behavioral Specification (2010, background): “Examples of implementation-oriented specification languages are JML [8] and Spec# [7].”
A Simple and Practical Approach to Unit Testing: The JML and JUnit Way (2002, methodology): “The code we have been writing is part of a tool suite for the Java Modeling Language (JML) [7].”
ESC/Java2: Uniting ESC/Java and JML (2004, neutral): “The activities of several groups [1,3,19,27,28] generated a number of tools that work with JML.”