Hussain, Faraz (2009) Enhancing a behavioral interface specification language with temporal logic features. Masters thesis, Computer Science, Iowa State University.
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.
|Keywords:||JML, temporal, specification, assertion checkers, java modeling language, assertions, invariants, logics of programs, preconditions, postconditions|
|Subjects:||Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)|
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
|Deposited by:||Faraz Hussain on 14 September 2010|
Contact site administrator at: firstname.lastname@example.org