A Run-time Assertion Checker for Java using JML
Abhay Bhorkar · Iowa State University Digital Repository (Iowa State University) · 2000
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.