org.jmlspecs.models
Class JMLValueSet_JML_Test.TestIsProperSuperset

java.lang.Object
  junit.framework.Assert
      junit.framework.TestCase
          org.jmlspecs.models.JMLValueSet_JML_TestData
              org.jmlspecs.models.JMLValueSet_JML_Test
                  org.jmlspecs.models.JMLValueSet_JML_Test.OneTest
                      org.jmlspecs.models.JMLValueSet_JML_Test.TestIsProperSuperset

All Implemented Interfaces:

junit.framework.Test

Enclosing class:

JMLValueSet_JML_Test

protected static class JMLValueSet_JML_Test.TestIsProperSuperset

extends JMLValueSet_JML_Test.OneTest

Test for the isProperSuperset method.

Nested Class Summary

 

Nested classes inherited from class org.jmlspecs.models.JMLValueSet_JML_Test

JMLValueSet_JML_Test.OneTest, JMLValueSet_JML_Test.TestChoose, JMLValueSet_JML_Test.TestClone, JMLValueSet_JML_Test.TestContainsAll, JMLValueSet_JML_Test.TestConvertFrom, JMLValueSet_JML_Test.TestDifference, JMLValueSet_JML_Test.TestElements, JMLValueSet_JML_Test.TestEquals, JMLValueSet_JML_Test.TestHas, JMLValueSet_JML_Test.TestHashCode, JMLValueSet_JML_Test.TestInsert, JMLValueSet_JML_Test.TestInt_size, JMLValueSet_JML_Test.TestIntersection, JMLValueSet_JML_Test.TestIsEmpty, JMLValueSet_JML_Test.TestIsProperSubset, JMLValueSet_JML_Test.TestIsProperSuperset, JMLValueSet_JML_Test.TestIsSubset, JMLValueSet_JML_Test.TestIsSuperset, JMLValueSet_JML_Test.TestIterator, JMLValueSet_JML_Test.TestJMLValueSet, JMLValueSet_JML_Test.TestPowerSet, JMLValueSet_JML_Test.TestRemove, JMLValueSet_JML_Test.TestSingleton, JMLValueSet_JML_Test.TestToArray, JMLValueSet_JML_Test.TestToBag, JMLValueSet_JML_Test.TestToSequence, JMLValueSet_JML_Test.TestToString, JMLValueSet_JML_Test.TestUnion

 

Field Summary
private  JMLValueSet	s2           Argument s2

 

Fields inherited from class org.jmlspecs.models.JMLValueSet_JML_Test.OneTest

result

 

Fields inherited from class org.jmlspecs.models.JMLValueSet_JML_TestData

 

Fields inherited from class junit.framework.TestCase

 

Constructor Summary

JMLValueSet_JML_Test.TestIsProperSuperset(JMLValueSet receiver$, JMLValueSet s2)           Initialize this instance.

 

Method Summary
protected  void	doCall()
protected  String	failMessage(JMLAssertionError e$)

 

Methods inherited from class org.jmlspecs.models.JMLValueSet_JML_Test.OneTest

run, runTest

 

Methods inherited from class org.jmlspecs.models.JMLValueSet_JML_Test

addTestSuiteForEachMethod, charToString, main, suite

 

Methods inherited from class org.jmlspecs.models.JMLValueSet_JML_TestData

emptyTestSuiteFor, overallTestSuite, vjava_lang_ObjectIter, vjava_util_CollectionIter, vorg_jmlspecs_models_JMLCollectionIter, vorg_jmlspecs_models_JMLTypeIter, vorg_jmlspecs_models_JMLValueSetIter

 

Methods inherited from class junit.framework.TestCase

countTestCases, createResult, getName, run, runBare, setName, setUp, tearDown, toString

 

Methods inherited from class junit.framework.Assert

assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertFalse, assertFalse, assertNotNull, assertNotNull, assertNotSame, assertNotSame, assertNull, assertNull, assertSame, assertSame, assertTrue, assertTrue, fail, fail

 

Methods inherited from class java.lang.Object

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

 

Field Detail

s2

private JMLValueSet s2

Argument s2

JMLValueSet_JML_Test.TestIsProperSuperset

public JMLValueSet_JML_Test.TestIsProperSuperset(JMLValueSet receiver$,
                                                 JMLValueSet s2)

Initialize this instance.

doCall

protected void doCall()
               throws Throwable

Description copied from class: JMLValueSet_JML_Test.OneTest

Call the method to be tested with the appropriate arguments.

Throws:

Throwable

failMessage

protected String failMessage(JMLAssertionError e$)

Description copied from class: JMLValueSet_JML_Test.OneTest

Format the error message for a test failure, based on the method's arguments.