org.jmlspecs.jmlunit
Class JMLTestRunner

java.lang.Object
  junit.runner.BaseTestRunner
      junit.textui.TestRunner
          org.jmlspecs.jmlunit.JMLTestRunner

All Implemented Interfaces:

junit.framework.TestListener

public class JMLTestRunner

extends junit.textui.TestRunner

A JML/JUnit test runner class. This class refines JUnit's text-based test runner class TestRunner and provides a command line based tool to run tests.

 java org.jmlspecs.jmlunit.JMLTestRunner [-M] [-R] [-testMode] [-list] [-wait] TestCaseClass
 

When the -wait command line argument is given JMLTestRunner waits until the users types RETURN.

JMLTestRunner prints a trace as the tests are executed followed by a summary at the end. In addition to the summary by TestRunner, it produces JML/JUnit specific test results such as the total number of test cases and the number of meaningful test cases.

More information about meaningless test cases is printed by using the -M flag. The -R flag can be used to suppress reporting coverage information which is normally printed after successful runs.

The -list option simply lists the tests by name, in order, without running them. The -testMode option does not print out time information so that test output is consistent from run to run.

Version:

$Revision: 1.26 $

Author:

Yoonsik Cheon, Gary T. Leavens, David Cok

Class Specifications

invariant (* printer == super.fPrinter *);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Nested Class Summary
static class	JMLTestRunner.JmlResultPrinter

 

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
protected static boolean	listMode           If true, then instead of running tests, they are simply listed by name in order.
private  JMLTestRunner.JmlResultPrinter	printer
protected static boolean	showCoverage           If true, then information about the coverage of tests is printed at the end of the JUnit run.
protected static boolean	showMeaninglessCases           If true, then information about the cases declared meaningless is printed at the end of the JUnit run.
protected static boolean	testMode           If true, then no information that varies from test run to test run (such as elapsed time) is printed.

 

Fields inherited from class junit.textui.TestRunner

EXCEPTION_EXIT, FAILURE_EXIT, SUCCESS_EXIT

 

Fields inherited from class junit.runner.BaseTestRunner

SUITE_METHODNAME

 

Constructor Summary
	JMLTestRunner()           Constructs a JMLTestRunner using System.out for all output.
	JMLTestRunner(PrintStream writer)           Constructs a JMLTestRunner using the given stream for all the output.
private	JMLTestRunner(JMLTestRunner.JmlResultPrinter printer)           Constructs a TestRunner using the given ResultPrinter all the output

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
protected  junit.framework.TestResult	createTestResult()           Creates a test result object to be used for a test run.
junit.framework.TestResult	doRun(junit.framework.Test suite, boolean wait)           Performs test execution and print test report.
static void	main(String[] args)           Performs test execution for the user-specified testcase class.
static junit.framework.TestResult	run(junit.framework.Test suite)           Runs a single test and collects its results.
static void	runAndWait(junit.framework.Test suite)           Runs a single test and waits until the user types RETURN.

 

Methods inherited from class junit.textui.TestRunner

doRun, getLoader, pause, run, runFailed, setPrinter, start, testEnded, testFailed, testStarted

 

Methods inherited from class junit.runner.BaseTestRunner

addError, addFailure, clearStatus, elapsedTimeAsString, endTest, extractClassName, getFilteredTrace, getFilteredTrace, getPreference, getPreference, getPreferences, getTest, inVAJava, loadSuiteClass, processArguments, savePreferences, setLoading, setPreference, setPreferences, showStackRaw, startTest, truncate, useReloadingTestSuiteLoader

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

showMeaninglessCases

protected static boolean showMeaninglessCases

If true, then information about the cases declared meaningless is printed at the end of the JUnit run.

showCoverage

protected static boolean showCoverage

If true, then information about the coverage of tests is printed at the end of the JUnit run.

testMode

protected static boolean testMode

If true, then no information that varies from test run to test run (such as elapsed time) is printed.

listMode

protected static boolean listMode

If true, then instead of running tests, they are simply listed by name in order.

printer

private JMLTestRunner.JmlResultPrinter printer

JMLTestRunner

public JMLTestRunner()

Constructs a JMLTestRunner using System.out for all output.

JMLTestRunner

public JMLTestRunner(PrintStream writer)

Constructs a JMLTestRunner using the given stream for all the output.

JMLTestRunner

private JMLTestRunner(JMLTestRunner.JmlResultPrinter printer)

Constructs a TestRunner using the given ResultPrinter all the output

main

public static void main(String[] args)

Performs test execution for the user-specified testcase class. The name of a TestData class (a subclass of junit.TestCase) must be given as an argument. If this class defines a static suite method it will be invoked and the returned test is run. Otherwise all the methods starting with "test" having no arguments are run.

 
 java org.jmlspecs.jmlunit.JMLTestRunner [-M] [-R] [-testMode] [-wait] TestCaseClass 
 

run

public static junit.framework.TestResult run(junit.framework.Test suite)

Runs a single test and collects its results. This method can be used to start a test run from a program, e.g.

 public static void main (String[] args) {
     org.jmlspecs.jmlunit.JMLTestRunner.run(suite());
 }
 

runAndWait

public static void runAndWait(junit.framework.Test suite)

Runs a single test and waits until the user types RETURN.

doRun

public junit.framework.TestResult doRun(junit.framework.Test suite,
                                        boolean wait)

Performs test execution and print test report. This method is overridden here to produce a JML-specific summary report. The method print of the class ResultPrinter is package-visible, thus all these troubles of overriding.

Overrides:

doRun in class junit.textui.TestRunner

createTestResult

protected junit.framework.TestResult createTestResult()

Creates a test result object to be used for a test run.

Overrides:

createTestResult in class junit.textui.TestRunner