JML

org.jmlspecs.jmlunit
Class JMLTestResult

java.lang.Object
  extended byjunit.framework.TestResult
      extended byorg.jmlspecs.jmlunit.JMLTestResult

public class JMLTestResult
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 the number of meaningless test runs (e.g., test inputs causing precondition violations).

Version:
$Revision: 1.8 $
Author:
Yoonsik Cheon, Gary T. Leavens

Field Summary
private  HashSet auditors
           
private static String line_sep
           
private  int meaninglessCount
          Counter for the total number of meaningless JML test runs.
private  StringBuffer meaninglessInformation
          StringBuffer that contains information on all of the meaningless test runs.
 
Fields inherited from class junit.framework.TestResult
fErrors, fFailures, fListeners, fRunTests
 
Constructor Summary
JMLTestResult()
          Constructs a new JMLTestResult object.
 
Method Summary
 void addJMLListener(JMLTestListener jmlListener)
          Add the argument to the set of JML listeners (only) Such listeners will only be notified also of meaningless test executions, and will not receive the notifications normal TestListeners receive.
 void addListener(JMLTestListener jmlListener)
          Add the argument to the set of JML listeners and the set of listeners maintained by the superclass.
 void addMeaningless(junit.framework.Test test)
          Increments the total number of JML test runs that are meaningless (i.e., those with entry precondition violations), and notifies any JMLTestListeners.
 void append(String msg)
          Appends information about meaningless test cases.
 int meaninglessCount()
          Returns the total number of JML meaningless test runs.
 String meaninglessTestCaseInfo()
          Returns information about all of the meaningless test cases.
 
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
 

Field Detail

auditors

private HashSet auditors

line_sep

private static final String line_sep

meaninglessCount

private int meaninglessCount
Counter for the total number of meaningless JML test runs.

 public invariant meaninglessCount >= 0;
 


meaninglessInformation

private StringBuffer meaninglessInformation
StringBuffer that contains information on all of the meaningless test runs.

Constructor Detail

JMLTestResult

public JMLTestResult()
Constructs a new JMLTestResult object.

Method Detail

addJMLListener

public void addJMLListener(JMLTestListener jmlListener)
Add the argument to the set of JML listeners (only) Such listeners will only be notified also of meaningless test executions, and will not receive the notifications normal TestListeners receive.

See Also:
addListener(JMLTestListener)

addListener

public void addListener(JMLTestListener jmlListener)
Add the argument to the set of JML listeners and the set of listeners maintained by the superclass. Such listeners will be notified also of meaningless test executions, in addition to the notifications normal TestListeners receive.

See Also:
addJMLListener(JMLTestListener)

addMeaningless

public void addMeaningless(junit.framework.Test test)
Increments the total number of JML test runs that are meaningless (i.e., those with entry precondition violations), and notifies any JMLTestListeners.

 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.


meaninglessCount

public int meaninglessCount()
Returns the total number of JML meaningless test runs.

 ensures \result == meaninglessCount;
 


JML

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.