Package org.jmlspecs.jmlunit

Generates JUnit test classes from JML specifications.

See:
Description

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.
JMLTestRunner.JmlResultPrinter
JntGUI	This class is automatically generated from JntGUI.gui and contains member fields corresponding to tool-specific GUI specifications.
JntMessages
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.
Main.Main$1
Main.Main$2
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.

• Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In Boris Magnusson (ed.), ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pages 231-255.
  Also Department of Computer Science, Iowa State University, TR #01-12a, November 2001, revised March 2002. [abstract] [postscript] [PDF]

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.