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 {@link java.lang.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.
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.
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 {@link java.util.Collection}, because that interface assumes collections are mutable objects. These can be divided into to three broad classes: the ``object'', ``value'', and ``equals'' 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.
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.
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.
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.
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.
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 {@link java.lang.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.
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.
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.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.
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.
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 org.jmlspecs.lang.JMLDataGroup