Uses of Package
org.jmlspecs.models

Packages that use org.jmlspecs.models

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.
org.jmlspecs.models.resolve	This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models.
org.jmlspecs.samples.digraph	This package contains samples of JML specifications for directed graphs.
org.jmlspecs.samples.dirobserver	This package contains samples of JML specifications that illustrate issues in component-based programming relating to callbacks and JML's model program feature.
org.jmlspecs.samples.jmlkluwer	This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design".
org.jmlspecs.samples.prelimdesign	This package contains samples of JML specifications from the paper Preliminary Design of JML.
org.jmlspecs.samples.table	This package contains samples of JML specifications relating to tables.

Classes in org.jmlspecs.models used by org.jmlspecs.models

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_TestData
Supply test data for the JML and JUnit based testing of Person.

JMLCollection
Common protocol of the JML model collection types.

JMLComparable
JMLTypes with an compareTo operation, as in Comparable.

JMLDouble
A reflection of Double that implements JMLType.

JMLEnumeration
A combination of JMLType and java.util.Enumeration.

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_TestData
Supply test data for the JML and JUnit based testing of Person.

JMLInfiniteInteger
Infinite precision integers with an plus and minus infinity.

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_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_TestData
Supply test data for the JML and JUnit based testing of Person.

JMLIterator
A combination of JMLType and java.util.Iterator.

JMLListEqualsNode
An implementation class used in various models.

JMLListException
Exceptions from JML List types.

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_TestData
Supply test data for the JML and JUnit based testing of Person.

JMLLong
A reflection of Long that implements JMLType.

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.

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

JMLObjectType
Objects that are containers of object references.

JMLObjectValuePair
Pairs of Object and JMLType, used in the types JMLObjectToValueRelation and JMLObjectToValueMap.

JMLSequenceException
Index out of bounds exceptions from JML Sequence types.

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_TestData
Supply test data for the JML and JUnit based testing of Person.

JMLType
Objects with a clone and equals method.

JMLTypeException
An exception class used in bad formatting exceptions.

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

JMLValueType
Objects that contain values.

JMLValueValuePair
Pairs of JMLType and JMLType, used in the types JMLValueToValueRelation and JMLValueToValueMap.

Classes in org.jmlspecs.models used by org.jmlspecs.models.resolve

JMLCollection
Common protocol of the JML model collection types.

JMLIterator
A combination of JMLType and java.util.Iterator.

JMLObjectSequence
Sequences of objects.

JMLObjectSequenceEnumerator
An enumerator for sequences of objects.

JMLType
Objects with a clone and equals method.

Classes in org.jmlspecs.models used by org.jmlspecs.samples.digraph

JMLType
Objects with a clone and equals method.

Classes in org.jmlspecs.models used by org.jmlspecs.samples.dirobserver

JMLType
Objects with a clone and equals method.

Classes in org.jmlspecs.models used by org.jmlspecs.samples.jmlkluwer

JMLType
Objects with a clone and equals method.

Classes in org.jmlspecs.models used by org.jmlspecs.samples.prelimdesign

JMLType
Objects with a clone and equals method.

Classes in org.jmlspecs.models used by org.jmlspecs.samples.table

JMLType
Objects with a clone and equals method.