org.jmlspecs.jmlunit
Class JMLTestRunner.JmlResultPrinter

java.lang.Object
  junit.textui.ResultPrinter
      org.jmlspecs.jmlunit.JMLTestRunner.JmlResultPrinter

All Implemented Interfaces:

junit.framework.TestListener

Enclosing class:

JMLTestRunner

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

hashValue

 

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

sizeOfWarningBlanks

private static final String sizeOfWarningBlanks

A number of blanks the size of the chr string "WARNING: ".

writer

private PrintStream writer

JMLTestRunner.JmlResultPrinter

JMLTestRunner.JmlResultPrinter(PrintStream writer)

print

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.

printFooter

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.

Overrides:

printFooter in class junit.textui.ResultPrinter