archives

A Run-time Assertion Checker for Java using JML


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Bhorkar, Abhay (2000) A Run-time Assertion Checker for Java using JML. Technical Report TR00-08, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

Abstract

A Run-time Assertion Checker for Java using JML
by
Abhay Bhorkar
Abstract
The Java Modeling Language (JML) is a behavioral interface
specification language tailored for specifying Java modules. This
paper describes a source-to-source translation tool that takes a JML
specification and Java source code for a module and produces source
code that checks assertions at run-time. It describes issues unique to
JML, including specification-only variables, refinement, specification
inheritance, and privacy. It also describes the design and
implementation of the translation tool.
Keywords: run-time assertion checking, precondition checking,
model-based specification, behavioral interface specification
language, behavioral subtyping, refinement, formal specification
languages, Eiffel, JML, Java.
1999 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications --- languages, tools, JML;
D.2.4 [Software Engineering]
Software/Program Verification --- Assertion checkers, class invariants,
formal methods,
programming by contract, reliability, tools, JML;
D.2.5 [Software Engineering]
Testing and Debugging --- Debugging aids;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, invariants, pre- and post-conditions,
specification techniques;
Copyright (c) 2000 by Iowa State University

Subjects:All uncategorized technical reports
ID code:00000219
Deposited by:Staff Account on 15 May 2000



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