org.jmlspecs.jmlunit
Class JMLTestResult

java.lang.Object
  junit.framework.TestResult
      org.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

Class Specifications

public invariant this.meaninglessCount >= 0; private represents jmlListeners <- org.jmlspecs.models.JMLObjectSet.convertFrom(this.auditors);

Specifications inherited from class Object

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

Model Field Summary
JMLObjectSet	jmlListeners

 

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
private  HashSet	auditors
private static String	line_sep
[spec_public] private  int	meaninglessCount
[spec_public] 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.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

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

 

Model Field Detail

jmlListeners

public JMLObjectSet jmlListeners

Specifications: non_null
datagroup contains: auditors

auditors

private HashSet auditors

Specifications: non_null
is in groups: jmlListeners

line_sep

private static final String line_sep

meaninglessCount

private int meaninglessCount

Specifications: spec_public

meaninglessInformation

private StringBuffer meaninglessInformation

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

Specifications: spec_public

JMLTestResult

public JMLTestResult()

Constructs a new JMLTestResult object.

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)

Specifications:

requires jmlListener != null;
assignable jmlListeners;
ensures this.jmlListeners.has(jmlListener);

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)

Specifications:

requires jmlListener != null;
assignable objectState, jmlListeners;
ensures this.jmlListeners.has(jmlListener);

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.

Specifications:

ensures this.meaninglessCount == \old(this.meaninglessCount+1);
assignable (* the changable state in each listener *);
assignable meaninglessCount;
ensures this.meaninglessCount == \old(this.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.

Specifications:

ensures \result == this.meaninglessCount;