edu.utep.cs.utjml.rat
Class RatTestResult

java.lang.Object
  junit.framework.TestResult
      edu.utep.cs.utjml.rat.RatTestResult

public class RatTestResult
extends junit.framework.TestResult

A class for collecting the results of executing test cases. In addition to test failures and errors collected by the superclass, this class accumulates JML-specific test information such as total and meaningless test runs (e.g., test inputs causing precondition violations).

Version:

$Revision: 1.1 $

Author:

Yoonsik Cheon

Field Summary

Fields inherited from class junit.framework.TestResult

fErrors, fFailures, fListeners, fRunTests

Constructor Summary

RatTestResult(RatTestRunner.JmlResultPrinter printer)
Constructs a new RatTestResult object.

Method Summary

void	append(String msg) Appends information about meaningless test cases.
void	incMeaninglessCount() Increments the total number of JML test runs that are meaningless (e.g., precondition violations and null receivers).
void	incTotalCount() Increments the total number of JML test runs.
int	meaninglessCount() Returns the total number of JML meaningless test runs.
String	meaninglessTestCaseInfo() Returns information about all of the meaningless test cases.
void	startJmlTest() Prints a dot for a JML/JUnit test case.
int	totalCount() Returns the total number of JML test runs.

Methods inherited from class junit.framework.TestResult

addError, addFailure, addListener, endTest, errorCount, errors, failureCount, failures, removeListener, run, runCount, runProtected, shouldStop, startTest, stop, wasSuccessful

Methods inherited from class java.lang.Object

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

Constructor Detail

RatTestResult

public RatTestResult(RatTestRunner.JmlResultPrinter printer)

Constructs a new RatTestResult object.

Method Detail

incTotalCount

public void incTotalCount()

Increments the total number of JML test runs.

 ensures totalCount == \old(totalCount + 1);
 

incMeaninglessCount

public void incMeaninglessCount()

Increments the total number of JML test runs that are meaningless (e.g., precondition violations and null receivers).

 ensures meaninglessCount == \old(meaninglessCount + 1);
 

append

public void append(String msg)

Appends information about meaningless test cases.

meaninglessTestCaseInfo

public String meaninglessTestCaseInfo()

Returns information about all of the meaningless test cases.

totalCount

public int totalCount()

Returns the total number of JML test runs.

 ensures \result == totalCount;
 

meaninglessCount

public int meaninglessCount()

Returns the total number of JML meaningless test runs.

 ensures \result == meaninglessCount;
 

startJmlTest

public void startJmlTest()

Prints a dot for a JML/JUnit test case.