Package org.jmlspecs.jmlunit

Generates JUnit test classes from JML specifications.


Interface Summary
Constants An interface for defining constants.
JMLTestListener A listener for test progress that takes into account meaningless test results (in which an entry precondition was false).

Class Summary
FancyTabbedPrintWriter A more convenient print writer.
JMLTestResult A class for collecting the results of executing test cases.
JMLTestRunner A JML/JUnit test runner class.
JntGUI This class is automatically generated from JntGUI.gui and contains member fields corresponding to tool-specific GUI specifications.
JntOptions This class is automatically generated from JntOptions.opt and contains member fields corresponding to command-line options.
Main A class implementing the entry point of the JML/JUnit test oracle generator.
TestClassGenerator A class for generating JML/JUnit test driver classes.
TestClassGenerator.NameGenerator A class for generating unique names for test methods.
TestClassGenerator.Parameter A simple data structure class for storing information about a formal parameter.
TestDataClassGenerator A class for generating JML/JUnit test data classes.

Package org.jmlspecs.jmlunit Description

Generates JUnit test classes from JML specifications. The idea behind jmlunit is to use JML's runtime assertion checker as a test oracle and use JUnit as a testing framework. The generated test classes send messages to objects of the Java classes under test; they catch assertion violation exceptions from test cases that pass an initial precondition check. Such assertion violation exceptions are used to decide if the code failed to meet its specification, and hence that the test failed. If the class under test satisfies its interface specification for some particular input values, no such exceptions will be thrown, and that particular test execution succeeds. So the automatically generated test code serves as a test oracle whose behavior is derived from the specified behavior of the target class. The user is still responsible for generating test data; however the generated test classes make it easy for the user to add test data.

For a class T, jmlunit generates a JUnit test class T_JML_TestData (if it does not already exist) and a subclass T_JML_Test. The user can add test data to the T_JML_TestDataclass, as directed in the comments of that class. If the user wishes, that class can also be used to define additional tests and the fixture methods setUp and tearDown.

Related Documentation

The idea of using a formal specification language's runtime assertion checker as a test oracle and combining JML and JUnit has been discussed in the following paper.

Coding Notes

The source code for the JML*.java files in this package uses the GNU Lesser General Public License, since it is part of the JML runtime libraries.


JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.