Abstract

The Java Modeling Language (JML) is a Behavioral Interface Specification Language (BISL) that can be used to specify the behavior of Java modules. Several tools have been developed for JML, such as the JML (type) checker, JML Runtime Assertion Checker (RAC), ESC/Java2, LOOP and so on. The RAC can be used to translate JML specifications into Java code so that the specifications can be checked at run-time. In this thesis we describe how two recent enhancements to JML have been formally defined and implemented in the RAC. The RAC semantics (of the newly added functionality) is presented as a large-step operational semantics. An overview of the RAC design is given so as to provide a better understanding of the context in which the enhancements have been made. The main enhancement to be realized is the added support for arbitrary precision integers in JML specification expressions and model method bodies. We also present prototypical implementation of an alternate semantics for JML assertions that has only very recently been published.