Date of Award
Master of Science
Gary T. Leavens
Specification languages help programmers write correct programs and also aid efforts for dynamically checking a software implementation with respect to its desired specifications. Most mainstream specification languages primarily deal with a program's functional behavior. However, for certain applications it is more natural and intuitive to be able to express a system's temporal properties.
This thesis enhances the capabilities of the Java Modeling Language (JML), a behavioral interface specification language, by incorporating temporal logic constructs. The temporal specification grammar used is a modification of the JML temporal extension proposed by K. Trentelman and M. Huisman in their paper "Extending JML Specifications with Temporal Logic".
I have modified jmlc, the runtime assertion checker for the Java Modeling Language, so that it also generates runtime assertion checking code to dynamically check a program's temporal specifications.
Hussain, Faraz, "Enhancing a behavioral interface specification language with temporal logic features" (2009). Graduate Theses and Dissertations. 10342.