Preliminary Design of JML: A Behavioral Interface Specification Language for Java

Date
2006-01-01
Authors
Leavens, Gary
Baker, Albert
Ruby, Clyde
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions. This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.

Description

Copyright © 1998-2006 Iowa State University

This document is part of JML and is distributed under the terms of the GNU General Public License as published by the Free Sofware Foundation; either version 2, or (at your option) any later version.

Keywords
Behavioral interface specification, Java, JML, Eiffel, Larch, model-based specification, assertion, precondition, postcondition, frame
Citation
DOI
Source
Collections