JML and its Unit Testing Tool
Dr Gary
Leavens
Iowa State University
Date:
Time:
Place: 1225
Engineering
Host: L. Dillon
Abstract:
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,
Biography:
Gary T. Leavens is a professor of
computer science at