JML and its Unit Testing Tool
Iowa State University
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.
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,
Gary T. Leavens is a professor of
computer science at