Enhancing a behavioral interface specification language
		     with temporal logic features
				  by
			    Faraz Hussain

			       Abstract 

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.

2006 CR Categories:
D.2.1 [Software Engineering] Requirements/Specifications 
      --- languages, methodologies; 
D.2.4 [Software Engineering] Software/Program Verification 
      --- assertion checkers, formal methods, programming by contract; 
D.3.3 [Programming Languages] Language Constructs and Features 
      --- abstract data types, data types and structures, patterns;
F.3.1 [Logics and Meanings of Programs] 
      Specifying and Verifying and Reasoning about Programs 
      --- assertions, invariants, logics of programs,
          pre- and post-conditions, specification techniques.

Copyright (c) 2009 Faraz Hussain