archives

JML: notations and tools supporting detailed design in Java


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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.

Full text available as:Postscript

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