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

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