UTJML

edu.utep.cs.utjml.tgen
Class TcgTestResult

java.lang.Object
  extended by junit.framework.TestResult
      extended by edu.utep.cs.utjml.tgen.TcgTestResult

public class TcgTestResult
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.3 $
Author:
Yoonsik Cheon

Field Summary
 
Fields inherited from class junit.framework.TestResult
fErrors, fFailures, fListeners, fRunTests
 
Constructor Summary
TcgTestResult(TcgTestRunner.JmlResultPrinter printer)
          Constructs a new TcgTestResult 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

TcgTestResult

public TcgTestResult(TcgTestRunner.JmlResultPrinter printer)
Constructs a new TcgTestResult 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.


UTJML

UTJML is Copyright (C) 2004-2006 by University of Texas at El Paso 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 JML project.