A Runtime Assertion Checker for the Java Modeling Language (JML)

Thumbnail Image
Date
2002-04-01
Authors
Cheon, Yoonsik
Leavens, Gary
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Computer Science
Abstract

Debugging is made difficult by the need to precisely describe what each piece of the software is supposed to do, and to write code to defend modules against the errors of other modules; if this is not done it is difficult to assign blame to a small part of the program when things go wrong. Similarly, unit testing also needs precise descriptions of behavior, and is made difficult by the need to write test oracles. However, debugging and testing consume a significant fraction of the cost of software development and maintenance efforts. Inadequate debugging and testing also contribute to quality problems. We describe a runtime assertion checker for the Java Modeling Language (JML) that helps in assigning blame during debugging and in automatic generation of test oracles. It represents a significant advance over the current state of the art, because it can deal with very abstract specifications which hide representation details, and other features such as quantifiers, and inheritance of specifications. Yet JML specifications have a syntax that is easily understood by programmers. Thus, JML's runtime assertion checker has the potential for decreasing the cost of debugging and testing.

Comments

To appear in International Conference on Software Engineering Research and Practice (SERP) 2002, Las Vegas, Nevada, USA, June 24-27, 2002. Copyright © Computer Science Research, Education, and Application (CSREA) Press, 2002.

Description
Keywords
Citation
DOI
Source
Subject Categories
Copyright
Collections