Adapting JML to generic types and Java 1.6
David R. Cok · 2008
Despite the current effort to implement the Java Modeling Language for Java 1.5, and in particular for generic types, there has been no analysis of the effect of such a transition on JML itself, nor of what language changes should be implemented to take best advantage of the features of current Java. This paper analyzes the interactions between JML and the new features of Java 1.5 and 1.6, and it proposes appropriate changes to JML. Many implementation details for JML tools can be handled by choosing an existing Java 1.5+ compiler as a base; however, there are adjustments to the typing of JML expressions that would be appropriate, and there are issues needing careful attention arising from refinements, autoboxing, lock ordering operations, specification of enhanced for loops, type erasure, and the runtime execution of specifications involving type parameters. The features are implemented experimentally in