Class JMLTestRunner.JmlResultPrinter

  extended byjunit.textui.ResultPrinter
      extended byorg.jmlspecs.jmlunit.JMLTestRunner.JmlResultPrinter
All Implemented Interfaces:
Enclosing class:

public static class JMLTestRunner.JmlResultPrinter
extends junit.textui.ResultPrinter

Class Specifications
invariant (* writer == super.fWriter *);

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
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 static String sizeOfWarningBlanks
          A number of blanks the size of the chr string "WARNING: ".
private  PrintStream writer
Fields inherited from class junit.textui.ResultPrinter
Constructor Summary
(package private) JMLTestRunner.JmlResultPrinter(PrintStream writer)
Model Method Summary
Model methods inherited from class java.lang.Object
Method Summary
 void print(junit.framework.TestResult result, long runTime)
          Prints test report inluding a JML-specific summary.
 void printFooter(junit.framework.TestResult result)
          Prints the footer of the test report.
Methods inherited from class junit.textui.ResultPrinter
addError, addFailure, elapsedTimeAsString, endTest, getWriter, printDefect, printDefectHeader, printDefects, printDefectTrace, printErrors, printFailures, printHeader, startTest
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail


private static final String sizeOfWarningBlanks
A number of blanks the size of the chr string "WARNING: ".


private PrintStream writer
Constructor Detail


JMLTestRunner.JmlResultPrinter(PrintStream writer)
Method Detail


public void print(junit.framework.TestResult result,
                  long runTime)
Prints test report inluding a JML-specific summary. This method is redefined here as the superclass's is package-visible.


public void printFooter(junit.framework.TestResult result)
Prints the footer of the test report. This method is overridden here to print JML-specific summary footer.

printFooter in class junit.textui.ResultPrinter


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.