Authors

Abhay Bhorkar

Publication Date

5-1-2000

Technical Report Number

TR00-08

Subjects

Data, Computing Methodologies, Software

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.

Share

COinS