Publication Date

11-1998

Technical Report Number

TR98-06b

Subjects

Software, Theory of Computation, Computing Methodologies, General Literature

Abstract

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used by working software engineers, and requires only modest mathematical training. To achieve this goal, JML uses Eiffel-style assertion syntax combined with the model-based approach to specifications typified by VDM and Larch. However, JML supports quantifiers, specification-only variables, frame conditions, and other enhancements that make it more expressive for specification than Eiffel. This paper discusses the goals of JML, the overall approach, and describes the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.

Comments

Copyright © 1998 by Gary T. Leavens, Albert L. Baker and Clyde Ruby.

Share

COinS