org.jmlspecs.jmlunit.strategies
Class ConstructorFailed

java.lang.Object
  org.jmlspecs.jmlunit.strategies.ConstructorFailed

All Implemented Interfaces:

junit.framework.Test

public class ConstructorFailed

extends Object

implements junit.framework.Test

A class that stores an exception that occured during test suite construction as a JUnit test, and when the test is run makes the problem a failure.

Author:

Gary T. Leavens

Class Specifications

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
[spec_public] private  Throwable	cause           The problem that occurred.
private  String	failmsg           The failure message for failures raised by this class.

 

Constructor Summary

ConstructorFailed(Throwable ex)           Initialize this object

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
int	countTestCases()
void	run(junit.framework.TestResult result)           Add a failure corresponding to cause to the result object.

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

cause

private final Throwable cause

The problem that occurred.

Specifications: spec_public non_null

failmsg

private final String failmsg

The failure message for failures raised by this class.

ConstructorFailed

public ConstructorFailed(Throwable ex)

Initialize this object

Specifications:

requires ex != null;
assignable cause;
ensures this.cause == ex;

countTestCases

public int countTestCases()

Specified by:

countTestCases in interface junit.framework.Test

run

public void run(junit.framework.TestResult result)

Add a failure corresponding to cause to the result object.

Specified by:

run in interface junit.framework.Test