JML

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

JML

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.