Class ConstructorFailed

  extended byorg.jmlspecs.jmlunit.strategies.ConstructorFailed
All Implemented Interfaces:

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.

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


private final Throwable cause
The problem that occurred.

Specifications: spec_public non_null


private final String failmsg
The failure message for failures raised by this class.

Constructor Detail


public ConstructorFailed(Throwable ex)
Initialize this object

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


public int countTestCases()
Specified by:
countTestCases in interface junit.framework.Test


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


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.