JML: notations and tools supporting detailed design in Java

Leavens, Gary T., Leino, K. Rustan M., Poll, Erik, Ruby, Clyde and Jacobs, Bart (2000) JML: notations and tools supporting detailed design in Java. Technical Report TR00-15, Department of Computer Science, Iowa State University.

Abstract

JML: notations and tools
supporting detailed design in Java
by
Gary T. Leavens, K. Rustan M. Leino, Erik Poll,
Clyde Ruby, and Bart Jacobs
Abstract
JML is a notation for specifying the detailed design of Java classes
and interfaces.  JML's assertions are stated using a slight extension
of Java's expression syntax.  This should make it easy to use.  Tools
for JML aid in static analysis, verification, and run-time debugging
of Java code.
Keywords: Behavioral interface specification language, detailed design
notation, Java language, JML language, ESC/Java, LOOP.
1999 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications --- languages, tools, JML,
ESC/Java, LOOP;
D.2.4 [Software Engineering]
Software/Program Verification --- Class invariants,
correctness proofs, formal methods,
programming by contract, reliability, tools, JML;
D.2.7 [Software Engineering]
Distribution, Maintenance, and Enhancement --- Documentation;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, invariants, logics of programs,
pre- and post-conditions, specification techniques;
To appear in OOPSLA 2000 Companion, Minneapolis, Minnesota,
Copyright (c) ACM 2000.


Subjects:
All uncategorized technical reports


ID code:
00000231
Deposited by:
Staff Account on 28 August 2000





Contact site administrator at: ssg@cs.iastate.edu