Skip to main content

JML and its Unit Testing Tool

Dr Gary Leavens
Iowa State University

Date:  Friday, Feb 3, 2006 
Place: 1225 Engineering

Host: L. Dillon


The Java Modeling Language (JML) is a behavioral interface specification language tailored to Java. This talk will give some background on JML, focusing on how JML's treatment of software contracts differs from Eiffel. JML supports a wide variety of tools, including a unit testing tool that will be the focus of the second part of the talk.

The unit testing tool in JML makes writing unit tests easier. It uses JML's runtime assertion checker to decide whether methods are working correctly, thus automating the writing of unit test oracles. These oracles can be easily combined with hand-written test data. Instead of writing test oracle code, the programmer writes formal specifications (e.g., pre- and postconditions). This makes the programmer's task easier, because specifications are more concise and abstract than the equivalent test code, and hence more readable and maintainable. Furthermore, by using specifications in testing, specification errors are quickly discovered, so the specifications are more likely to provide useful documentation and inputs to other tools. The talk will explain the idea and also our experience with this kind of specification-based testing.

This talk is based in part on joint work with Yoonsik Cheon. The work is supported in part by the NSF under grant CCR-0097907, CCR-0113181, CCF-0428078, and CCF-0429567. The original version of the unit testing tool work appeared in the ECOOP 2002 conference, Malaga, Spain, June 2002, pp. 231-255, LNCS volume 2374. More information on JML can be found at


Gary T. Leavens is a professor of computer science at Iowa State University in Ames, Iowa . He has taught there since receiving his Ph.D. from MIT in 1989. Before that he worked at Bell Telephone Laboratories in Denver Colorado as a member of technical staff. Professor Leavens's research interests include programming and specification language design and semantics, program verification, and formal methods, with an emphasis on the object-oriented and aspect-oriented paradigms. His best known work in the area of formal methods is in behavioral subtyping (much of it joint with Don Pigozzi and Krishna Kishore Dhara) and the design of the specification languages Larch/Smalltalk, Larch/C++, and JML (joint with Yoonsik Cheon and Clyde Ruby). His best known work on language design and semantics is in semantics and type checking for multiple dispatch languages (joint with Craig Chambers, Todd Millstein, and Curtis Clifton) such as MultiJava. See