Package org.jmlspecs.models

This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package.

See:
Description

Interface Summary

JMLCollection	Common protocol of the JML model collection types.
JMLComparable	JMLTypes with an compareTo operation, as in Comparable.
JMLEnumeration	A combination of JMLType and java.util.Enumeration.
JMLInfiniteInteger	Infinite precision integers with an plus and minus infinity.
JMLIterator	A combination of JMLType and java.util.Iterator.
JMLObjectType	Objects that are containers of object references.
JMLType	Objects with a clone and equals method.
JMLValueType	Objects that contain values.

Class Summary

JMLArrayOps	Array Operations that are useful for specifications.
JMLByte	A reflection of Byte that implements JMLType.
JMLChar	A reflection of Character that implements JMLType.
JMLChar_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLChar.
JMLChar_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLChar_JML_Test.TestCharValue	Test for the charValue method.
JMLChar_JML_Test.TestClone	Test for the clone method.
JMLChar_JML_Test.TestCompareTo	Test for the compareTo method.
JMLChar_JML_Test.TestDividedBy	Test for the dividedBy method.
JMLChar_JML_Test.TestEquals	Test for the equals method.
JMLChar_JML_Test.TestGetChar	Test for the getChar method.
JMLChar_JML_Test.TestGreaterThan	Test for the greaterThan method.
JMLChar_JML_Test.TestGreaterThanOrEqualTo	Test for the greaterThanOrEqualTo method.
JMLChar_JML_Test.TestHashCode	Test for the hashCode method.
JMLChar_JML_Test.TestIntValue	Test for the intValue method.
JMLChar_JML_Test.TestJMLChar	Test for the JMLChar contructor.
JMLChar_JML_Test.TestJMLChar$1	Test for the JMLChar contructor.
JMLChar_JML_Test.TestJMLChar$2	Test for the JMLChar contructor.
JMLChar_JML_Test.TestLessThan	Test for the lessThan method.
JMLChar_JML_Test.TestLessThanOrEqualTo	Test for the lessThanOrEqualTo method.
JMLChar_JML_Test.TestMinus	Test for the minus method.
JMLChar_JML_Test.TestPlus	Test for the plus method.
JMLChar_JML_Test.TestRemainderBy	Test for the remainderBy method.
JMLChar_JML_Test.TestTimes	Test for the times method.
JMLChar_JML_Test.TestToString	Test for the toString method.
JMLChar_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLDouble	A reflection of Double that implements JMLType.
JMLEnumerationToIterator	A wrapper that makes any JMLEnumeration into a JMLIterator that does not support the remove operation.
JMLEqualsBag	Bags (i.e., multisets) of objects.
JMLEqualsBagEntry	Internal class used in the implementation of JMLEqualsBag.
JMLEqualsBagEntryNode	Internal class used in the implementation of JMLEqualsBag.
JMLEqualsBagEnumerator	Enumerators for bags (i.e., multisets) of objects.
JMLEqualsEqualsPair	Pairs of Object and Object, used in the types JMLEqualsToEqualsRelation and JMLEqualsToEqualsMap.
JMLEqualsObjectPair	Pairs of Object and Object, used in the types JMLEqualsToObjectRelation and JMLEqualsToObjectMap.
JMLEqualsSequence	Sequences of objects.
JMLEqualsSequenceEnumerator	An enumerator for sequences of objects.
JMLEqualsSet	Sets of objects.
JMLEqualsSetEnumerator	An enumerator for sets of objects.
JMLEqualsToEqualsMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of Object.
JMLEqualsToEqualsRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of Object.
JMLEqualsToEqualsRelationEnumerator	Enumerator for pairs of keys of type Object to values of type Object that form the associations in a relation.
JMLEqualsToEqualsRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLEqualsToObjectMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of Object.
JMLEqualsToObjectRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of Object.
JMLEqualsToObjectRelationEnumerator	Enumerator for pairs of keys of type Object to values of type Object that form the associations in a relation.
JMLEqualsToObjectRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLEqualsToValueMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of JMLType.
JMLEqualsToValueRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of JMLType.
JMLEqualsToValueRelationEnumerator	Enumerator for pairs of keys of type Object to values of type JMLType that form the associations in a relation.
JMLEqualsToValueRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLEqualsValuePair	Pairs of Object and JMLType, used in the types JMLEqualsToValueRelation and JMLEqualsToValueMap.
JMLFiniteInteger	Arbitrary precision integers with a finite value.
JMLFloat	A reflection of Float that implements JMLType.
JMLFloat_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLFloat.
JMLFloat_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLFloat_JML_Test.TestApproximatelyEqualTo	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$1	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$2	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$3	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$4	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$5	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestApproximatelyEqualTo$6	Test for the approximatelyEqualTo method.
JMLFloat_JML_Test.TestClone	Test for the clone method.
JMLFloat_JML_Test.TestCompareTo	Test for the compareTo method.
JMLFloat_JML_Test.TestDividedBy	Test for the dividedBy method.
JMLFloat_JML_Test.TestEquals	Test for the equals method.
JMLFloat_JML_Test.TestFloatValue	Test for the floatValue method.
JMLFloat_JML_Test.TestGetFloat	Test for the getFloat method.
JMLFloat_JML_Test.TestGreaterThan	Test for the greaterThan method.
JMLFloat_JML_Test.TestGreaterThanOrEqualTo	Test for the greaterThanOrEqualTo method.
JMLFloat_JML_Test.TestHashCode	Test for the hashCode method.
JMLFloat_JML_Test.TestIsInfinite	Test for the isInfinite method.
JMLFloat_JML_Test.TestIsNaN	Test for the isNaN method.
JMLFloat_JML_Test.TestIsZero	Test for the isZero method.
JMLFloat_JML_Test.TestIsZero$1	Test for the isZero method.
JMLFloat_JML_Test.TestJMLFloat	Test for the JMLFloat contructor.
JMLFloat_JML_Test.TestJMLFloat$1	Test for the JMLFloat contructor.
JMLFloat_JML_Test.TestJMLFloat$2	Test for the JMLFloat contructor.
JMLFloat_JML_Test.TestJMLFloat$3	Test for the JMLFloat contructor.
JMLFloat_JML_Test.TestJMLFloat$4	Test for the JMLFloat contructor.
JMLFloat_JML_Test.TestLessThan	Test for the lessThan method.
JMLFloat_JML_Test.TestLessThanOrEqualTo	Test for the lessThanOrEqualTo method.
JMLFloat_JML_Test.TestMinus	Test for the minus method.
JMLFloat_JML_Test.TestNegated	Test for the negated method.
JMLFloat_JML_Test.TestPlus	Test for the plus method.
JMLFloat_JML_Test.TestRemainderBy	Test for the remainderBy method.
JMLFloat_JML_Test.TestTimes	Test for the times method.
JMLFloat_JML_Test.TestToString	Test for the toString method.
JMLFloat_JML_Test.TestWithinEpsilonOf	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$1	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$2	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$3	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$4	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$5	Test for the withinEpsilonOf method.
JMLFloat_JML_Test.TestWithinEpsilonOf$6	Test for the withinEpsilonOf method.
JMLFloat_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLInfiniteInteger_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLInfiniteInteger.
JMLInfiniteInteger_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLInfiniteInteger_JML_Test.TestAbs	Test for the abs method.
JMLInfiniteInteger_JML_Test.TestAdd	Test for the add method.
JMLInfiniteInteger_JML_Test.TestClone	Test for the clone method.
JMLInfiniteInteger_JML_Test.TestCompareTo	Test for the compareTo method.
JMLInfiniteInteger_JML_Test.TestDivide	Test for the divide method.
JMLInfiniteInteger_JML_Test.TestDoubleValue	Test for the doubleValue method.
JMLInfiniteInteger_JML_Test.TestEquals	Test for the equals method.
JMLInfiniteInteger_JML_Test.TestFiniteValue	Test for the finiteValue method.
JMLInfiniteInteger_JML_Test.TestFloatValue	Test for the floatValue method.
JMLInfiniteInteger_JML_Test.TestGreaterThan	Test for the greaterThan method.
JMLInfiniteInteger_JML_Test.TestGreaterThanOrEqualTo	Test for the greaterThanOrEqualTo method.
JMLInfiniteInteger_JML_Test.TestHashCode	Test for the hashCode method.
JMLInfiniteInteger_JML_Test.TestIsFinite	Test for the isFinite method.
JMLInfiniteInteger_JML_Test.TestLessThan	Test for the lessThan method.
JMLInfiniteInteger_JML_Test.TestLessThanOrEqualTo	Test for the lessThanOrEqualTo method.
JMLInfiniteInteger_JML_Test.TestMax	Test for the max method.
JMLInfiniteInteger_JML_Test.TestMin	Test for the min method.
JMLInfiniteInteger_JML_Test.TestMod	Test for the mod method.
JMLInfiniteInteger_JML_Test.TestMultiply	Test for the multiply method.
JMLInfiniteInteger_JML_Test.TestNegate	Test for the negate method.
JMLInfiniteInteger_JML_Test.TestPow	Test for the pow method.
JMLInfiniteInteger_JML_Test.TestRemainder	Test for the remainder method.
JMLInfiniteInteger_JML_Test.TestSignum	Test for the signum method.
JMLInfiniteInteger_JML_Test.TestSubtract	Test for the subtract method.
JMLInfiniteInteger_JML_Test.TestToString	Test for the toString method.
JMLInfiniteInteger_JML_Test.TestToString$1	Test for the toString method.
JMLInfiniteInteger_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLInfiniteIntegerClass	Class with common code to implement JMLInfiniteInteger.
JMLInteger	A reflection of Integer that implements JMLType.
JMLInteger_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLInteger.
JMLInteger_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLInteger_JML_Test.TestClone	Test for the clone method.
JMLInteger_JML_Test.TestCompareTo	Test for the compareTo method.
JMLInteger_JML_Test.TestDividedBy	Test for the dividedBy method.
JMLInteger_JML_Test.TestEquals	Test for the equals method.
JMLInteger_JML_Test.TestGetInteger	Test for the getInteger method.
JMLInteger_JML_Test.TestGreaterThan	Test for the greaterThan method.
JMLInteger_JML_Test.TestGreaterThanOrEqualTo	Test for the greaterThanOrEqualTo method.
JMLInteger_JML_Test.TestHashCode	Test for the hashCode method.
JMLInteger_JML_Test.TestIntValue	Test for the intValue method.
JMLInteger_JML_Test.TestJMLInteger	Test for the JMLInteger contructor.
JMLInteger_JML_Test.TestJMLInteger$1	Test for the JMLInteger contructor.
JMLInteger_JML_Test.TestJMLInteger$2	Test for the JMLInteger contructor.
JMLInteger_JML_Test.TestJMLInteger$3	Test for the JMLInteger contructor.
JMLInteger_JML_Test.TestLessThan	Test for the lessThan method.
JMLInteger_JML_Test.TestLessThanOrEqualTo	Test for the lessThanOrEqualTo method.
JMLInteger_JML_Test.TestMinus	Test for the minus method.
JMLInteger_JML_Test.TestNegated	Test for the negated method.
JMLInteger_JML_Test.TestPlus	Test for the plus method.
JMLInteger_JML_Test.TestRemainderBy	Test for the remainderBy method.
JMLInteger_JML_Test.TestTimes	Test for the times method.
JMLInteger_JML_Test.TestToString	Test for the toString method.
JMLInteger_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLListEqualsNode	An implementation class used in various models.
JMLListObjectNode	An implementation class used in various models.
JMLListValueNode	An implementation class used in various models.
JMLListValueNode_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLListValueNode.
JMLListValueNode_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLListValueNode_JML_Test.TestAppend	Test for the append method.
JMLListValueNode_JML_Test.TestClone	Test for the clone method.
JMLListValueNode_JML_Test.TestConcat	Test for the concat method.
JMLListValueNode_JML_Test.TestCons	Test for the cons method.
JMLListValueNode_JML_Test.TestEquals	Test for the equals method.
JMLListValueNode_JML_Test.TestGetItem	Test for the getItem method.
JMLListValueNode_JML_Test.TestHas	Test for the has method.
JMLListValueNode_JML_Test.TestHashCode	Test for the hashCode method.
JMLListValueNode_JML_Test.TestHead	Test for the head method.
JMLListValueNode_JML_Test.TestHeadEquals	Test for the headEquals method.
JMLListValueNode_JML_Test.TestIndexOf	Test for the indexOf method.
JMLListValueNode_JML_Test.TestInsertBefore	Test for the insertBefore method.
JMLListValueNode_JML_Test.TestInt_length	Test for the int_length method.
JMLListValueNode_JML_Test.TestInt_size	Test for the int_size method.
JMLListValueNode_JML_Test.TestIsPrefixOf	Test for the isPrefixOf method.
JMLListValueNode_JML_Test.TestItemAt	Test for the itemAt method.
JMLListValueNode_JML_Test.TestJMLListValueNode	Test for the JMLListValueNode contructor.
JMLListValueNode_JML_Test.TestLast	Test for the last method.
JMLListValueNode_JML_Test.TestPrefix	Test for the prefix method.
JMLListValueNode_JML_Test.TestPrepend	Test for the prepend method.
JMLListValueNode_JML_Test.TestRemove	Test for the remove method.
JMLListValueNode_JML_Test.TestRemoveItemAt	Test for the removeItemAt method.
JMLListValueNode_JML_Test.TestRemoveLast	Test for the removeLast method.
JMLListValueNode_JML_Test.TestRemovePrefix	Test for the removePrefix method.
JMLListValueNode_JML_Test.TestReplaceItemAt	Test for the replaceItemAt method.
JMLListValueNode_JML_Test.TestReverse	Test for the reverse method.
JMLListValueNode_JML_Test.TestToString	Test for the toString method.
JMLListValueNode_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLLong	A reflection of Long that implements JMLType.
JMLMath	A JML class that implements methods equivalent to those available in Math but that are defined over \bigint and \real instead.
JMLModelObjectSet	A collection of object sets for use in set comprehensions.
JMLModelValueSet	A collection of value sets for use in set comprehensions.
JMLNegativeInfinity	Negative Infinity.
JMLNullSafe	A class with static methods that safely work with null objects.
JMLNullSafe_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLNullSafe.
JMLNullSafe_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLNullSafe_JML_Test.TestEquals	Test for the equals method.
JMLNullSafe_JML_Test.TestHashCode	Test for the hashCode method.
JMLNullSafe_JML_Test.TestToString	Test for the toString method.
JMLNullSafe_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLObjectBag	Bags (i.e., multisets) of objects.
JMLObjectBagEntry	Internal class used in the implementation of JMLObjectBag.
JMLObjectBagEntryNode	Internal class used in the implementation of JMLObjectBag.
JMLObjectBagEnumerator	Enumerators for bags (i.e., multisets) of objects.
JMLObjectEqualsPair	Pairs of Object and Object, used in the types JMLObjectToEqualsRelation and JMLObjectToEqualsMap.
JMLObjectObjectPair	Pairs of Object and Object, used in the types JMLObjectToObjectRelation and JMLObjectToObjectMap.
JMLObjectSequence	Sequences of objects.
JMLObjectSequenceEnumerator	An enumerator for sequences of objects.
JMLObjectSet	Sets of objects.
JMLObjectSetEnumerator	An enumerator for sets of objects.
JMLObjectToEqualsMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of Object.
JMLObjectToEqualsRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of Object.
JMLObjectToEqualsRelationEnumerator	Enumerator for pairs of keys of type Object to values of type Object that form the associations in a relation.
JMLObjectToEqualsRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLObjectToObjectMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of Object.
JMLObjectToObjectRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of Object.
JMLObjectToObjectRelation_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLObjectToObjectRelation.
JMLObjectToObjectRelation_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLObjectToObjectRelation_JML_Test.TestAdd	Test for the add method.
JMLObjectToObjectRelation_JML_Test.TestAssociations	Test for the associations method.
JMLObjectToObjectRelation_JML_Test.TestClone	Test for the clone method.
JMLObjectToObjectRelation_JML_Test.TestCompose	Test for the compose method.
JMLObjectToObjectRelation_JML_Test.TestCompose$1	Test for the compose method.
JMLObjectToObjectRelation_JML_Test.TestDifference	Test for the difference method.
JMLObjectToObjectRelation_JML_Test.TestDomain	Test for the domain method.
JMLObjectToObjectRelation_JML_Test.TestDomainElements	Test for the domainElements method.
JMLObjectToObjectRelation_JML_Test.TestElementImage	Test for the elementImage method.
JMLObjectToObjectRelation_JML_Test.TestElements	Test for the elements method.
JMLObjectToObjectRelation_JML_Test.TestEquals	Test for the equals method.
JMLObjectToObjectRelation_JML_Test.TestHas	Test for the has method.
JMLObjectToObjectRelation_JML_Test.TestHas$1	Test for the has method.
JMLObjectToObjectRelation_JML_Test.TestHas$2	Test for the has method.
JMLObjectToObjectRelation_JML_Test.TestHashCode	Test for the hashCode method.
JMLObjectToObjectRelation_JML_Test.TestImage	Test for the image method.
JMLObjectToObjectRelation_JML_Test.TestImagePairs	Test for the imagePairs method.
JMLObjectToObjectRelation_JML_Test.TestImagePairSet	Test for the imagePairSet method.
JMLObjectToObjectRelation_JML_Test.TestInsert	Test for the insert method.
JMLObjectToObjectRelation_JML_Test.TestInt_size	Test for the int_size method.
JMLObjectToObjectRelation_JML_Test.TestIntersection	Test for the intersection method.
JMLObjectToObjectRelation_JML_Test.TestInverse	Test for the inverse method.
JMLObjectToObjectRelation_JML_Test.TestInverseElementImage	Test for the inverseElementImage method.
JMLObjectToObjectRelation_JML_Test.TestInverseImage	Test for the inverseImage method.
JMLObjectToObjectRelation_JML_Test.TestIsaFunction	Test for the isaFunction method.
JMLObjectToObjectRelation_JML_Test.TestIsDefinedAt	Test for the isDefinedAt method.
JMLObjectToObjectRelation_JML_Test.TestIsEmpty	Test for the isEmpty method.
JMLObjectToObjectRelation_JML_Test.TestIterator	Test for the iterator method.
JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation	Test for the JMLObjectToObjectRelation contructor.
JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation$1	Test for the JMLObjectToObjectRelation contructor.
JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation$2	Test for the JMLObjectToObjectRelation contructor.
JMLObjectToObjectRelation_JML_Test.TestRange	Test for the range method.
JMLObjectToObjectRelation_JML_Test.TestRangeElements	Test for the rangeElements method.
JMLObjectToObjectRelation_JML_Test.TestRemove	Test for the remove method.
JMLObjectToObjectRelation_JML_Test.TestRemove$1	Test for the remove method.
JMLObjectToObjectRelation_JML_Test.TestRemoveFromDomain	Test for the removeFromDomain method.
JMLObjectToObjectRelation_JML_Test.TestRestrictDomainTo	Test for the restrictDomainTo method.
JMLObjectToObjectRelation_JML_Test.TestRestrictRangeTo	Test for the restrictRangeTo method.
JMLObjectToObjectRelation_JML_Test.TestSingleton	Test for the singleton method.
JMLObjectToObjectRelation_JML_Test.TestSingleton$1	Test for the singleton method.
JMLObjectToObjectRelation_JML_Test.TestToBag	Test for the toBag method.
JMLObjectToObjectRelation_JML_Test.TestToFunction	Test for the toFunction method.
JMLObjectToObjectRelation_JML_Test.TestToSequence	Test for the toSequence method.
JMLObjectToObjectRelation_JML_Test.TestToSet	Test for the toSet method.
JMLObjectToObjectRelation_JML_Test.TestToString	Test for the toString method.
JMLObjectToObjectRelation_JML_Test.TestUnion	Test for the union method.
JMLObjectToObjectRelation_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLObjectToObjectRelationEnumerator	Enumerator for pairs of keys of type Object to values of type Object that form the associations in a relation.
JMLObjectToObjectRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLObjectToValueMap	Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of JMLType.
JMLObjectToValueRelation	Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of JMLType.
JMLObjectToValueRelationEnumerator	Enumerator for pairs of keys of type Object to values of type JMLType that form the associations in a relation.
JMLObjectToValueRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLObjectValuePair	Pairs of Object and JMLType, used in the types JMLObjectToValueRelation and JMLObjectToValueMap.
JMLPositiveInfinity	Positive Infinity.
JMLResources	Model variables for reasoning à la Eric Hehner.
JMLShort	A reflection of Short that implements JMLType.
JMLString	A reflection of String that implements JMLType.
JMLString_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLString.
JMLString_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLString_JML_Test.TestClone	Test for the clone method.
JMLString_JML_Test.TestCompareTo	Test for the compareTo method.
JMLString_JML_Test.TestCompareTo$1	Test for the compareTo method.
JMLString_JML_Test.TestConcat	Test for the concat method.
JMLString_JML_Test.TestConcat$1	Test for the concat method.
JMLString_JML_Test.TestConcat$2	Test for the concat method.
JMLString_JML_Test.TestEquals	Test for the equals method.
JMLString_JML_Test.TestEqualsIgnoreCase	Test for the equalsIgnoreCase method.
JMLString_JML_Test.TestEqualsIgnoreCase$1	Test for the equalsIgnoreCase method.
JMLString_JML_Test.TestHashCode	Test for the hashCode method.
JMLString_JML_Test.TestJMLString	Test for the JMLString contructor.
JMLString_JML_Test.TestJMLString$1	Test for the JMLString contructor.
JMLString_JML_Test.TestToString	Test for the toString method.
JMLString_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLValueBag	Bags (i.e., multisets) of values.
JMLValueBagEntry	Internal class used in the implementation of JMLValueBag.
JMLValueBagEntryNode	Internal class used in the implementation of JMLValueBag.
JMLValueBagEnumerator	Enumerators for bags (i.e., multisets) of values.
JMLValueBagSpecs	Special behavior for JMLValueBag not shared by JMLObjectBag.
JMLValueEqualsPair	Pairs of JMLType and Object, used in the types JMLValueToEqualsRelation and JMLValueToEqualsMap.
JMLValueObjectPair	Pairs of JMLType and Object, used in the types JMLValueToObjectRelation and JMLValueToObjectMap.
JMLValueObjectPair_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLValueObjectPair.
JMLValueObjectPair_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLValueObjectPair_JML_Test.TestClone	Test for the clone method.
JMLValueObjectPair_JML_Test.TestEquals	Test for the equals method.
JMLValueObjectPair_JML_Test.TestHashCode	Test for the hashCode method.
JMLValueObjectPair_JML_Test.TestJMLValueObjectPair	Test for the JMLValueObjectPair contructor.
JMLValueObjectPair_JML_Test.TestKeyEquals	Test for the keyEquals method.
JMLValueObjectPair_JML_Test.TestToString	Test for the toString method.
JMLValueObjectPair_JML_Test.TestValueEquals	Test for the valueEquals method.
JMLValueObjectPair_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLValueSequence	Sequences of values.
JMLValueSequenceEnumerator	An enumerator for sequences of values.
JMLValueSequenceSpecs	Specical behavior for JMLValueSequence not shared by JMLObjectSequence.
JMLValueSet	Sets of values.
JMLValueSet_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLValueSet.
JMLValueSet_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLValueSet_JML_Test.TestChoose	Test for the choose method.
JMLValueSet_JML_Test.TestClone	Test for the clone method.
JMLValueSet_JML_Test.TestContainsAll	Test for the containsAll method.
JMLValueSet_JML_Test.TestConvertFrom	Test for the convertFrom method.
JMLValueSet_JML_Test.TestConvertFrom$1	Test for the convertFrom method.
JMLValueSet_JML_Test.TestConvertFrom$2	Test for the convertFrom method.
JMLValueSet_JML_Test.TestDifference	Test for the difference method.
JMLValueSet_JML_Test.TestElements	Test for the elements method.
JMLValueSet_JML_Test.TestEquals	Test for the equals method.
JMLValueSet_JML_Test.TestHas	Test for the has method.
JMLValueSet_JML_Test.TestHas$1	Test for the has method.
JMLValueSet_JML_Test.TestHashCode	Test for the hashCode method.
JMLValueSet_JML_Test.TestInsert	Test for the insert method.
JMLValueSet_JML_Test.TestInt_size	Test for the int_size method.
JMLValueSet_JML_Test.TestIntersection	Test for the intersection method.
JMLValueSet_JML_Test.TestIsEmpty	Test for the isEmpty method.
JMLValueSet_JML_Test.TestIsProperSubset	Test for the isProperSubset method.
JMLValueSet_JML_Test.TestIsProperSuperset	Test for the isProperSuperset method.
JMLValueSet_JML_Test.TestIsSubset	Test for the isSubset method.
JMLValueSet_JML_Test.TestIsSuperset	Test for the isSuperset method.
JMLValueSet_JML_Test.TestIterator	Test for the iterator method.
JMLValueSet_JML_Test.TestJMLValueSet	Test for the JMLValueSet contructor.
JMLValueSet_JML_Test.TestJMLValueSet$1	Test for the JMLValueSet contructor.
JMLValueSet_JML_Test.TestPowerSet	Test for the powerSet method.
JMLValueSet_JML_Test.TestRemove	Test for the remove method.
JMLValueSet_JML_Test.TestSingleton	Test for the singleton method.
JMLValueSet_JML_Test.TestToArray	Test for the toArray method.
JMLValueSet_JML_Test.TestToBag	Test for the toBag method.
JMLValueSet_JML_Test.TestToSequence	Test for the toSequence method.
JMLValueSet_JML_Test.TestToString	Test for the toString method.
JMLValueSet_JML_Test.TestUnion	Test for the union method.
JMLValueSet_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLValueSetEnumerator	An enumerator for sets of values.
JMLValueSetSpecs	Special behavior for JMLValueSet not shared by JMLObjectSet.
JMLValueToEqualsMap	Maps (i.e., binary relations that are functional) from non-null elements of JMLType to non-null elements of Object.
JMLValueToEqualsRelation	Binary relations (or set-valued functions) from non-null elements of JMLType to non-null elements of Object.
JMLValueToEqualsRelationEnumerator	Enumerator for pairs of keys of type JMLType to values of type Object that form the associations in a relation.
JMLValueToEqualsRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLValueToObjectMap	Maps (i.e., binary relations that are functional) from non-null elements of JMLType to non-null elements of Object.
JMLValueToObjectRelation	Binary relations (or set-valued functions) from non-null elements of JMLType to non-null elements of Object.
JMLValueToObjectRelationEnumerator	Enumerator for pairs of keys of type JMLType to values of type Object that form the associations in a relation.
JMLValueToObjectRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLValueToValueMap	Maps (i.e., binary relations that are functional) from non-null elements of JMLType to non-null elements of JMLType.
JMLValueToValueMap_JML_Test	Automatically-generated test driver for JML and JUnit based testing of JMLValueToValueMap.
JMLValueToValueMap_JML_Test.OneTest	A JUnit test object that can run a single test method.
JMLValueToValueMap_JML_Test.TestAdd	Test for the add method.
JMLValueToValueMap_JML_Test.TestApply	Test for the apply method.
JMLValueToValueMap_JML_Test.TestAssociations	Test for the associations method.
JMLValueToValueMap_JML_Test.TestClashReplaceUnion	Test for the clashReplaceUnion method.
JMLValueToValueMap_JML_Test.TestClone	Test for the clone method.
JMLValueToValueMap_JML_Test.TestCompose	Test for the compose method.
JMLValueToValueMap_JML_Test.TestCompose$1	Test for the compose method.
JMLValueToValueMap_JML_Test.TestCompose$2	Test for the compose method.
JMLValueToValueMap_JML_Test.TestCompose$3	Test for the compose method.
JMLValueToValueMap_JML_Test.TestDifference	Test for the difference method.
JMLValueToValueMap_JML_Test.TestDisjointUnion	Test for the disjointUnion method.
JMLValueToValueMap_JML_Test.TestDomain	Test for the domain method.
JMLValueToValueMap_JML_Test.TestDomainElements	Test for the domainElements method.
JMLValueToValueMap_JML_Test.TestElementImage	Test for the elementImage method.
JMLValueToValueMap_JML_Test.TestElements	Test for the elements method.
JMLValueToValueMap_JML_Test.TestEquals	Test for the equals method.
JMLValueToValueMap_JML_Test.TestExtend	Test for the extend method.
JMLValueToValueMap_JML_Test.TestExtendUnion	Test for the extendUnion method.
JMLValueToValueMap_JML_Test.TestHas	Test for the has method.
JMLValueToValueMap_JML_Test.TestHas$1	Test for the has method.
JMLValueToValueMap_JML_Test.TestHas$2	Test for the has method.
JMLValueToValueMap_JML_Test.TestHashCode	Test for the hashCode method.
JMLValueToValueMap_JML_Test.TestImage	Test for the image method.
JMLValueToValueMap_JML_Test.TestImagePairs	Test for the imagePairs method.
JMLValueToValueMap_JML_Test.TestImagePairSet	Test for the imagePairSet method.
JMLValueToValueMap_JML_Test.TestInsert	Test for the insert method.
JMLValueToValueMap_JML_Test.TestInt_size	Test for the int_size method.
JMLValueToValueMap_JML_Test.TestIntersection	Test for the intersection method.
JMLValueToValueMap_JML_Test.TestInverse	Test for the inverse method.
JMLValueToValueMap_JML_Test.TestInverseElementImage	Test for the inverseElementImage method.
JMLValueToValueMap_JML_Test.TestInverseImage	Test for the inverseImage method.
JMLValueToValueMap_JML_Test.TestIsaFunction	Test for the isaFunction method.
JMLValueToValueMap_JML_Test.TestIsDefinedAt	Test for the isDefinedAt method.
JMLValueToValueMap_JML_Test.TestIsEmpty	Test for the isEmpty method.
JMLValueToValueMap_JML_Test.TestIterator	Test for the iterator method.
JMLValueToValueMap_JML_Test.TestJMLValueToValueMap	Test for the JMLValueToValueMap contructor.
JMLValueToValueMap_JML_Test.TestJMLValueToValueMap$1	Test for the JMLValueToValueMap contructor.
JMLValueToValueMap_JML_Test.TestJMLValueToValueMap$2	Test for the JMLValueToValueMap contructor.
JMLValueToValueMap_JML_Test.TestRange	Test for the range method.
JMLValueToValueMap_JML_Test.TestRangeElements	Test for the rangeElements method.
JMLValueToValueMap_JML_Test.TestRangeRestrictedTo	Test for the rangeRestrictedTo method.
JMLValueToValueMap_JML_Test.TestRemove	Test for the remove method.
JMLValueToValueMap_JML_Test.TestRemove$1	Test for the remove method.
JMLValueToValueMap_JML_Test.TestRemoveDomainElement	Test for the removeDomainElement method.
JMLValueToValueMap_JML_Test.TestRemoveFromDomain	Test for the removeFromDomain method.
JMLValueToValueMap_JML_Test.TestRestrictDomainTo	Test for the restrictDomainTo method.
JMLValueToValueMap_JML_Test.TestRestrictedTo	Test for the restrictedTo method.
JMLValueToValueMap_JML_Test.TestRestrictRangeTo	Test for the restrictRangeTo method.
JMLValueToValueMap_JML_Test.TestSingletonMap	Test for the singletonMap method.
JMLValueToValueMap_JML_Test.TestSingletonMap$1	Test for the singletonMap method.
JMLValueToValueMap_JML_Test.TestToBag	Test for the toBag method.
JMLValueToValueMap_JML_Test.TestToFunction	Test for the toFunction method.
JMLValueToValueMap_JML_Test.TestToSequence	Test for the toSequence method.
JMLValueToValueMap_JML_Test.TestToSet	Test for the toSet method.
JMLValueToValueMap_JML_Test.TestToString	Test for the toString method.
JMLValueToValueMap_JML_Test.TestUnion	Test for the union method.
JMLValueToValueMap_JML_TestData	Supply test data for the JML and JUnit based testing of Person.
JMLValueToValueRelation	Binary relations (or set-valued functions) from non-null elements of JMLType to non-null elements of JMLType.
JMLValueToValueRelationEnumerator	Enumerator for pairs of keys of type JMLType to values of type JMLType that form the associations in a relation.
JMLValueToValueRelationImageEnumerator	Enumerator for pairs of keys and their relational images.
JMLValueValuePair	Pairs of JMLType and JMLType, used in the types JMLValueToValueRelation and JMLValueToValueMap.
TestSuite	This class is automatically generated using org.multijava.util.testing.Main and is used to group a collection of JUnit tests for the local package and perhaps some subpackages.
TestSuite.TestSuite$1

Exception Summary

JMLListException	Exceptions from JML List types.
JMLMapException	Exceptions from JML Map types that indicate that the argument was illegal for this operation.
JMLNoSuchElementException	Missing element exception used by various JML collection types and enumerators.
JMLSequenceException	Index out of bounds exceptions from JML Sequence types.
JMLTypeException	An exception class used in bad formatting exceptions.

Package org.jmlspecs.models Description

This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package. An object is immutable if it has no time-varying state. The methods defined for objects of such types thus return other objects instead of making changes in place, as would occur for a mutable object.

The types of the immutable objects in this package are all pure, meaning that none of their specified methods have any user-visible side-effects (although a few inherited from Object do have side effects). Their pure methods, are designed for use in JML specifications. When using such methods you have to do something with the result returned by the method, as in functional programming. The original object's state is never changed by a pure method.

For example, to insert an element, e, into a set, s, one might execute s.insert(e), but this does not change the object s in any way; instead, it returns a set that contains all the old elements of s as well as e. At first you shouldn't worry about the time and space used to do make such a set -- remember that specifications are not mainly designed to be executed. If you're worried about efficiency, you aren't using the right frame of mind. (However, there are legitimate reasons to worry about the efficiency of executing specifications for testing and debugging purposes.)

The enumerator types (such as JMLObjectSetEnumerator) are mutable objects and some of their methods are not pure. These impure methods can't be used in specifications in JML.

Overview

There are several kinds of types in this package. These include various kinds of collections, reflections of types in java.lang that are useful as elements of these collections, and other types useful in various styles of specification. These are described below.

Collections

Perhaps the most useful model types are the various kinds of collections. All of the collections implement the interface JMLCollection. This interface is different from Collection, because that interface assumes collections are mutable objects. These can be divided into to three broad classes: the ``object'', ``value'', and ``equals'' collections.

Object collections

The object collections contain object references. These include JMLObjectSet, JMLObjectSequence, JMLObjectBag, and so on. All of these treat their elements as object references (addresses) and don't care about the values of these objects. For example, objects of type JMLObjectSet are sets of object references. When an object is inserted into such a set, it is not cloned. The equality test used by the has method uses Java's == operator to compare addresses of these objects.

Value collections

In contrast, the value collections, such as JMLValueSet, JMLValueSequence, and JMLValueBag, contain object values. The objects references stored in such a collection are merely representatives of the corresponding equivalence classes (of all objects with the same value). For example, objects of type JMLValueSet are sets of values. When an object is inserted into such a set, it is cloned, so that later changes to the object do not affect its value. The equality test used by the has method uses the .equals method of the object's class.

To support cloning, all of the value collection types contain elements that implement the JMLType interface. The requirement that the elements of a value collection implement this interface is an unfortunate limitation of this scheme, which is necessitated by Java's type system.

Equals Collections

The ``equals'' collections are hybrids of the object and value collections. They are collections of object identities, however, like the value collections, the operations all use Java's equals method to compare elements.

These types are inherently unsafe when the elements are mutable, because if the elements are mutated in ways that change their equivalence class (i.e., in ways that change the way that they compare with respect to the equals method), then the collection can be changed without invoking any of the elements of the collection. So it is best not to use such collections to relate pre- and post-states of methods, except when the elements are known not to be mutated.

Relations and Maps

The relation and map types come in nine (9) kinds. These relate either objects or values to either objects or values, and the objects may be compared using either == or the equals method For example, JMLObjectToValueRelation relates objects to values, using == to compare the left hand side objects, while JMLValueToObjectRelation relates objects to values, but uses the equals method to relate all elements.

Model Sets

The types JMLModelObjectSet and JMLModelValueSet are designed for use in JML's set comprehensions. They provide methods that return, for a given type, the set of all objects (or values) that type. The returned sets can then be filtered in a set comprehension. Note, however, that most of these methods are model methods, and will render assertions that use them nonexecutable.

Reflections of java.lang classes

Because of the need for types that implement the JMLType interface, this package also has reflections of various types in the java.lang package that implement the JMLType interface. For example, JMLShort is something like Short, but implements JMLType. Other such types are JMLInteger, JMLLong, JMLFloat, JMLDouble, JMLByte, JMLChar, and JMLString.

The numeric types that reflect types in java.lang, such as JMLShort, have one other advantage over their counterparts in java.lang. This advantage is that they also have methods to do arithmetic. For example, one can add and subtract objects of types JMLShort.

Types that support various specification styles

The type JMLInfiniteInteger is useful for specification à la Eric Hehner of time and space properties. Also useful for such purposes is JMLResources.

See also the package org.jmlspecs.models.resolve for types that support the RESOLVE specification style.

Convenience or Abbreviation Types

Several types are provided as conveniences and provide ways to shorten specifications of common idioms.

The type JMLArrayOps provides a operations to search for and count elements in arrays, using either == or the equals method for comparisons to the elements.

The type JMLNullSafe provides a static method that can perform equals on two objects that may be null. It also has methods that perform a toString or hashCode call on a possibly null object, returning a sensible result.

Specification Style

These types are intended to be bullet-proof; i.e., they are not designed for trusted clients. The reason is to help ensure the semantics of normal logic in assertion evaluation. That is, when a method's precondition is not met, an exception must be thrown, so that tools have a chance to catch the exception. Often this exception is actually specified behavior of the type, although for certain kinds of non null arguments and for some finiteness issues it suffices to make sure that the code will signal an exception, as opposed to specifying it.

The types are also intended to be used by both JML and ESC/Java. The reason for this is that we have used ESC/Java to help debug the specifications and implementations, and also that clients of these types might like to use ESC/Java. To this end the specifications contain some amount of redundancy (over and above the use of implications and examples). One of the ways that this shows up is in the use of the JML-only annotation markers of the form //+@ and /*+@ ... @+*/. We try to give a complete specification in the these annotations. The annotations marked by //@ and /*@ ... @*/ are intended mostly for ESC/Java. Some of these are quite redundant with the JML specifications, but not from the point of view of ESC/Java. We have tried to use non_null annotations in many cases to avoid some of this redundancy (although technically that still introduces some redundancy). We also use ESC/Java's nowarn pragmas in a few places, so that the code checks without any warnings.

Coding and the Makefiles

The main problem of coding in this package is how to avoid duplication between similar object, value, and equals types, for example between JMLObjectSet, JMLValueSet, and JMLEqualsSet. The way this is done is by coding these types once, and using a sed script to make the object, value, and equals versions of a type. For example, JMLObjectSet, JMLValueSet, and JMLEqualsSet are generated by the file JMLSet.java-generic using the script JMLSet.sh. This script also generates the related enumeration types: JMLObjectSetEnumerator, JMLValueSetEnumerator, and JMLEqualsSetEnumerator. Similarly, JMLObjectBag JMLValueBag, and JMLEqualsBag are generated by the file JMLBag.java-generic using the script JMLBag.sh. This script also generates the related bag enumeration types. Fragments of code that must be different in each type are defined using one of the strings in the sed script. Thus, it is important, when making changes to these types, to change the .java-generic file, instead of the generated .java files. The Makefile is designed to make the generated files read-only to prevent editing the wrong files.

Following the Makefile, use make generate to generate the files using the scripts.

To make sure that the pure types are pure, we only use final fields in the pure types. However, because the pure types have immutable objects, we can have clone return the receiver unchanged (since the aliasing can't be detected). Similarly, we play lots of other tricks with sharing to reduce space usage. Although time and space don't matter in some abstract sense, we make some concessions to efficiency, for the sake of the runtime assertion checker. However, when push comes to shove, the most important aspect of these types is their clarity and correctness.

In the test cases (the _JML_TestData.java files), we take advantage of the fact that the types are pure to speed up the JUnit-based testing. We also sometimes take advantage of the fact that other test data, particularly of type Object and JMLType are either not mutated by the tests or are actually immutable objects. (Note that new Object() produces a new immutable object!) Typically, the tests don't call any methods on the objects in the collections that would mutate them, so this is okay.

The source code for this package uses the GNU Lesser General Public License, since it is part of the JML runtime libraries.

Acknowledgments

These types were designed by Gary T. Leavens, Clyde Ruby, and Albert L. Baker, originally. Others contributing specifications are Curtis Clifton and Brandon Shilling. They have been refined under the supervision of Gary T. Leavens, with help from many JML users, including Rustan Leino, David Cok, Erik Poll, Jan Dockx, Roy Tan, and Marko van Doreen. David Cok in particular has made several improvements and deserves special thanks for his work; thanks David! The specification of the enumerators builds on work done for ESC/Java by Rustan Leino's group at HP SRC (which was Compaq SRC at the time).

At Iowa State, the development of JML was partially funded by a grant from Rockwell International Corporation and by the (US) National Science Foundation under grants CCR-9503168, CCR-9803843, CCR-0097907, and CCR-0113181.

See Also:

JMLDataGroup