JML Reloaded

Funded by Formal Methods Europe (FME)

Co-PI: Dr. Dan Zimmerman

The Java Modeling Language is a specification language for Java programs, supporting both a design by contract programming style (documenting class and method behavior and data consistency requirements with assertions) and more detailed logical modeling of system behavior. Many tools, such as the JML Common Tools (including a compiler, a runtime assertion checker, a documentation generator, a unit test generator, and other tools) and the ESC/Java static checker, understand the JML syntax and allow developers to incorporate the use of formal methods into their engineering process.

Unfortunately, as the Java programming language has evolved over the past several years (most notably with the addition of generic types), JML and its supporting tools have struggled to keep up with language changes. Most existing JML tools do not work with current Java code. Moreover, the JML tools that do work with current code have significant performance issues, and do not integrate well with development environments such as Eclipse, the industry-leading Open Source Java IDE.

The goal of the proposed project is to help coordinate JML tool development efforts among North American and European researchers, to modernize the JML tools for use with current (and future) versions of Java. This work will help make applied formal methods more attractive by making them accessible to thousands of Java programmers worldwide.