Dai, Kui (2005) Enhancements to the JML runtime assertion checker compiler. Masters thesis, Concordia University.
MR10284.pdf - Accepted Version
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.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering|
|Item Type:||Thesis (Masters)|
|Pagination:||viii, 79 leaves : ill. ; 29 cm.|
|Degree Name:||M. Comp. Sc.|
|Program:||Computer Science and Software Engineering|
|Thesis Supervisor(s):||Chalin, Patrice|
|Deposited By:||Concordia University Libraries|
|Deposited On:||18 Aug 2011 18:30|
|Last Modified:||05 Nov 2016 00:41|
Repository Staff Only: item control page