archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Cheon, Yoonsik and Leavens, Gary T. (2002) A Runtime Assertion Checker for the Java Modeling Language (JML). Technical Report TR #02-05, Department of Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

Abstract

Debugging is made difficult by the need to precisely describe what each part 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. JML's runtime assertion checker has the potential for decreasing the cost of debugging and testing. As a side benefit, the extra precision possible from formal specifications can also help increase the quality of software. Such specifications are also amenable to use by other tools, and in addition provide contracts that also serve as good documentation for detailed designs.

Keywords:runtime assertion checking, formal methods, formal interface specification, programming by contract, JML language, Java language
Subjects:Software: GENERAL
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Testing and Debugging
Software: PROGRAMMING LANGUAGES: Language Classifications
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000274
Deposited by:Yoonsik Cheon on 07 March 2002

Available Versions of This Paper



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