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

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
Field Detail

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
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)
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;

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.