| org.jmlspecs.models |
|
| Java Source File Name | Type | Comment |
| JMLArrayOps.java | Class | Array Operations that are useful for specifications.
version:
$Revision: 1.1 $
author:
Brandon Shilling
author:
Gary T. |
| JMLByte.java | Class | A reflection of
java.lang.Byte that implements
JMLType .
version:
$Revision: 1.3 $
author:
Gary T. |
| JMLChar.java | Class | A reflection of
java.lang.Character that implements
JMLType .
version:
$Revision: 1.2 $
author:
Curtis Clifton with extensive input from the JML Seminar
author:
at Iowa State University, June-July 1999.
author:
Gary T. |
| JMLCollection.java | Interface | Common protocol of the JML model collection types.
The use of elementType and containsNull in this specification
follows the ESC/Java specification of
java.util.Collection .
That is, these ghost fields are used by the user of the object to
state what types of objects are allowed to be added to the collection,
and hence what is guaranteed to be retrieved from the collection. |
| JMLComparable.java | Interface | JMLTypes with an compareTo operation, as in
java.lang.Comparable .
version:
$Revision: 1.1.1.1 $
author:
Gary T. |
| JMLDouble.java | Class | A reflection of
java.lang.Double that implements
JMLType .
version:
$Revision: 1.1 $
author:
Brandon Shilling
author:
Gary T. |
| JMLEnumeration.java | Interface | A combination of JMLType and java.util.Enumeration.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLEnumerationToIterator.java | Class | A wrapper that makes any
JMLEnumeration into a
JMLIterator that does not support the remove operation.
version:
$Revision: 1.1.1.1 $
author:
Gary T. |
| JMLEqualsBag.java | Class | Bags (i.e., multisets) of objects. |
| JMLEqualsBagEnumerator.java | Class | Enumerators for bags (i.e., multisets) of objects.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLEqualsEqualsPair.java | Class | Pairs of
Object and
Object , used in the types
JMLEqualsToEqualsRelation and
JMLEqualsToEqualsMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLEqualsObjectPair.java | Class | Pairs of
Object and
Object , used in the types
JMLEqualsToObjectRelation and
JMLEqualsToObjectMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLEqualsSequence.java | Class | |
| JMLEqualsSequenceEnumerator.java | Class | An enumerator for sequences of objects.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLEqualsSet.java | Class | Sets of objects. |
| JMLEqualsSetEnumerator.java | Class | An enumerator for sets of objects.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLEqualsToEqualsMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
Object . |
| JMLEqualsToEqualsRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
Object . |
| JMLEqualsToEqualsRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLEqualsToEqualsRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLEqualsToObjectMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
Object . |
| JMLEqualsToObjectRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
Object . |
| JMLEqualsToObjectRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLEqualsToObjectRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLEqualsToValueMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
JMLType . |
| JMLEqualsToValueRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
JMLType . |
| JMLEqualsToValueRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
JMLType that form the associations in a
relation.
version:
$Revision: 1.3 $
author:
Gary T. |
| JMLEqualsToValueRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLEqualsValuePair.java | Class | Pairs of
Object and
JMLType , used in the types
JMLEqualsToValueRelation and
JMLEqualsToValueMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLFiniteInteger.java | Class | Arbitrary precision integers with a finite value.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLFloat.java | Class | A reflection of
java.lang.Float that implements
JMLType .
version:
$Revision: 1.1 $
author:
Brandon Shilling
author:
Gary T. |
| JMLInfiniteInteger.java | Interface | Infinite precision integers with an plus and minus infinity.
This type is intended to support reasoning like that done by
Eric Hehner for the time behavior of programs. |
| JMLInfiniteIntegerClass.java | Class | Class with common code to implement JMLInfiniteInteger.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLInteger.java | Class | A reflection of
java.lang.Integer that implements
JMLType .
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLIterator.java | Interface | A combination of JMLType and java.util.Iterator.
None of these support the remove operation.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLListEqualsNode.java | Class | An implementation class used in various models. |
| JMLListException.java | Class | Exceptions from JML List types.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLListObjectNode.java | Class | An implementation class used in various models. |
| JMLListValueNode.java | Class | An implementation class used in various models. |
| JMLLong.java | Class | A reflection of
java.lang.Long that implements
JMLType .
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
_DomainType_ to non-null elements of
_RangeType_ . |
| JMLMapException.java | Class | Exceptions from JML Map types that indicate that the argument was
illegal for this operation.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLMath.java | Class | A JML class that implements methods equivalent to those available in
java.lang.Math but that are defined over \bigint and
\real instead. |
| JMLModelObjectSet.java | Class | A collection of object sets for use in set comprehensions. |
| JMLModelValueSet.java | Class | A collection of value sets for use in set comprehensions. |
| JMLNegativeInfinity.java | Class | Negative Infinity.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLNoSuchElementException.java | Class | Missing element exception used by various JML collection types and
enumerators.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLNullSafe.java | Class | A class with static methods that safely work with null objects.
version:
$Revision: 1.1 $
author:
Katie Becker and Gary T. |
| JMLObjectBag.java | Class | Bags (i.e., multisets) of objects. |
| JMLObjectBagEnumerator.java | Class | Enumerators for bags (i.e., multisets) of objects.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLObjectEqualsPair.java | Class | Pairs of
Object and
Object , used in the types
JMLObjectToEqualsRelation and
JMLObjectToEqualsMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLObjectObjectPair.java | Class | Pairs of
Object and
Object , used in the types
JMLObjectToObjectRelation and
JMLObjectToObjectMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLObjectSequence.java | Class | Sequences of objects. |
| JMLObjectSequenceEnumerator.java | Class | An enumerator for sequences of objects.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLObjectSet.java | Class | Sets of objects. |
| JMLObjectSetEnumerator.java | Class | An enumerator for sets of objects.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLObjectToEqualsMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
Object . |
| JMLObjectToEqualsRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
Object . |
| JMLObjectToEqualsRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLObjectToEqualsRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLObjectToObjectMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
Object . |
| JMLObjectToObjectRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
Object . |
| JMLObjectToObjectRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLObjectToObjectRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLObjectToValueMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
JMLType . |
| JMLObjectToValueRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
Object to non-null elements of
JMLType . |
| JMLObjectToValueRelationEnumerator.java | Class | Enumerator for pairs of keys of type
Object to
values of type
JMLType that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLObjectToValueRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLObjectType.java | Interface | Objects that are containers of object references.
It is the intention that classes that implement JMLObjectType be
"containers of objects", in the sense that the user is only
interested in the "object references", (addresses) themselves
as the elements in the container. |
| JMLObjectValuePair.java | Class | Pairs of
Object and
JMLType , used in the types
JMLObjectToValueRelation and
JMLObjectToValueMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLPositiveInfinity.java | Class | Positive Infinity.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLResources.java | Class | Model variables for reasoning à la Eric Hehner.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLSequenceException.java | Class | Index out of bounds exceptions from JML Sequence types.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLSetEnumerator.java | Class | An enumerator for sets of _ElemType_English_s.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLShort.java | Class | A reflection of
java.lang.Short that implements
JMLType .
version:
$Revision: 1.3 $
author:
Gary T. |
| JMLString.java | Class | A reflection of
java.lang.String that implements
JMLType .
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLType.java | Interface | Objects with a clone and equals method.
JMLObjectType and JMLValueType are refinements
for object and value containers (respectively).
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLTypeException.java | Class | An exception class used in bad formatting exceptions.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLValueBag.java | Class | Bags (i.e., multisets) of values. |
| JMLValueBagEnumerator.java | Class | Enumerators for bags (i.e., multisets) of values.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLValueBagSpecs.java | Class | Special behavior for JMLValueBag not shared by JMLObjectBag.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLValueEqualsPair.java | Class | Pairs of
JMLType and
Object , used in the types
JMLValueToEqualsRelation and
JMLValueToEqualsMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLValueObjectPair.java | Class | Pairs of
JMLType and
Object , used in the types
JMLValueToObjectRelation and
JMLValueToObjectMap .
In a pair the first element is called the "key" and the second
the "value". |
| JMLValueSequence.java | Class | |
| JMLValueSequenceEnumerator.java | Class | An enumerator for sequences of values.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLValueSequenceSpecs.java | Class | Specical behavior for JMLValueSequence not shared by JMLObjectSequence.
version:
$Revision: 1.3 $
author:
Gary T. |
| JMLValueSet.java | Class | Sets of values. |
| JMLValueSetEnumerator.java | Class | An enumerator for sets of values.
version:
$Revision: 1.1 $
author:
Gary T. |
| JMLValueSetSpecs.java | Class | Special behavior for JMLValueSet not shared by JMLObjectSet.
version:
$Revision: 1.3 $
author:
Gary T. |
| JMLValueToEqualsMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
JMLType to non-null elements of
Object . |
| JMLValueToEqualsRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
JMLType to non-null elements of
Object . |
| JMLValueToEqualsRelationEnumerator.java | Class | Enumerator for pairs of keys of type
JMLType to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLValueToEqualsRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLValueToObjectMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
JMLType to non-null elements of
Object . |
| JMLValueToObjectRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
JMLType to non-null elements of
Object . |
| JMLValueToObjectRelationEnumerator.java | Class | Enumerator for pairs of keys of type
JMLType to
values of type
Object that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLValueToObjectRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLValueToValueMap.java | Class | Maps (i.e., binary relations that are functional) from non-null
elements of
JMLType to non-null elements of
JMLType . |
| JMLValueToValueRelation.java | Class | Binary relations (or set-valued functions) from non-null elements
of
JMLType to non-null elements of
JMLType . |
| JMLValueToValueRelationEnumerator.java | Class | Enumerator for pairs of keys of type
JMLType to
values of type
JMLType that form the associations in a
relation.
version:
$Revision: 1.2 $
author:
Gary T. |
| JMLValueToValueRelationImageEnumerator.java | Class | Enumerator for pairs of keys and their relational images. |
| JMLValueType.java | Interface | Objects that contain values.
It is the intention that classes that implement JMLValueType provide a
"value semantics" for both clone() and equal(). |
| JMLValueValuePair.java | Class | Pairs of
JMLType and
JMLType , used in the types
JMLValueToValueRelation and
JMLValueToValueMap .
In a pair the first element is called the "key" and the second
the "value". |