|PREV PACKAGE NEXT PACKAGE||FRAMES NO FRAMES|
|AntisymmetricCompareTo||Objects with an antisymmetric compareTo operation.|
|AsymmetricCompareTo||Objects with an asymmetric compareTo operation.|
|CompareTo||Objects with a compareTo operation.|
|DenselyOrderedCompareTo||Objects with a dense order for their compareTo operation.|
|PartiallyOrderedCompareTo||Objects with a partial order for their compareTo operation.|
|PreorderedCompareTo||Objects with a preorder for their compareTo operation.|
|ReflexiveCompareTo||Objects with a reflexive compareTo operation.|
|StrictlyOrderedCompareTo||Objects with a strictly ordered compareTo operation.|
|StrictPartiallyOrderedCompareTo||Objects with a strict partially ordered compareTo operation.|
|SymmetricCompareTo||Objects with a symmetric compareTo operation.|
|TotalCompareTo||Objects whose compareTo operation is guaranteed not to throw an
|TotallyOrderedCompareTo||Objects with a totally ordered compareTo operation.|
|TotalPreorderedCompareTo||Objects with a total preorder for their compareTo operation.|
|TransitiveCompareTo||Objects with a transitive compareTo operation.|
|TrichotomousCompareTo||Objects with a trichotomous compareTo operation.|
|NaturalNumber||The natural numbers.|
|NaturalNumber_JML_Test||Automatically-generated test driver for JML and JUnit based testing of NaturalNumber.|
|NaturalNumber_JML_Test.OneTest||A JUnit test object that can run a single test method.|
|NaturalNumber_JML_Test.TestAdd||Test for the add method.|
|NaturalNumber_JML_Test.TestBigIntegerValue||Test for the bigIntegerValue method.|
|NaturalNumber_JML_Test.TestByteValue||Test for the byteValue method.|
|NaturalNumber_JML_Test.TestClone||Test for the clone method.|
|NaturalNumber_JML_Test.TestCompareTo||Test for the compareTo method.|
|NaturalNumber_JML_Test.TestCompareTo$1||Test for the compareTo method.|
|NaturalNumber_JML_Test.TestDivide||Test for the divide method.|
|NaturalNumber_JML_Test.TestDivides||Test for the divides method.|
|NaturalNumber_JML_Test.TestDoubleValue||Test for the doubleValue method.|
|NaturalNumber_JML_Test.TestEquals||Test for the equals method.|
|NaturalNumber_JML_Test.TestFloatValue||Test for the floatValue method.|
|NaturalNumber_JML_Test.TestGcd||Test for the gcd method.|
|NaturalNumber_JML_Test.TestHashCode||Test for the hashCode method.|
|NaturalNumber_JML_Test.TestIntValue||Test for the intValue method.|
|NaturalNumber_JML_Test.TestIsZero||Test for the isZero method.|
|NaturalNumber_JML_Test.TestLongValue||Test for the longValue method.|
|NaturalNumber_JML_Test.TestMax||Test for the max method.|
|NaturalNumber_JML_Test.TestMin||Test for the min method.|
|NaturalNumber_JML_Test.TestMod||Test for the mod method.|
|NaturalNumber_JML_Test.TestMultiply||Test for the multiply method.|
|NaturalNumber_JML_Test.TestNaturalNumber||Test for the NaturalNumber contructor.|
|NaturalNumber_JML_Test.TestNaturalNumber$1||Test for the NaturalNumber contructor.|
|NaturalNumber_JML_Test.TestNaturalNumber$2||Test for the NaturalNumber contructor.|
|NaturalNumber_JML_Test.TestPow||Test for the pow method.|
|NaturalNumber_JML_Test.TestPow$1||Test for the pow method.|
|NaturalNumber_JML_Test.TestRemainder||Test for the remainder method.|
|NaturalNumber_JML_Test.TestShiftLeft||Test for the shiftLeft method.|
|NaturalNumber_JML_Test.TestShiftRight||Test for the shiftRight method.|
|NaturalNumber_JML_Test.TestShortValue||Test for the shortValue method.|
|NaturalNumber_JML_Test.TestSuc||Test for the suc method.|
|NaturalNumber_JML_Test.TestSuc$1||Test for the suc method.|
|NaturalNumber_JML_Test.TestToString||Test for the toString method.|
|NaturalNumber_JML_Test.TestValueOf||Test for the valueOf method.|
|NaturalNumber_JML_TestData||Supply test data for the JML and JUnit based testing of Person.|
|StringOfObject||Sequences of non-null object identities.|
|StringOfObject_JML_Test||Automatically-generated test driver for JML and JUnit based testing of StringOfObject.|
|StringOfObject_JML_Test.OneTest||A JUnit test object that can run a single test method.|
|StringOfObject_JML_Test.TestAdd||Test for the add method.|
|StringOfObject_JML_Test.TestAddAfterIndex||Test for the addAfterIndex method.|
|StringOfObject_JML_Test.TestAddAll||Test for the addAll method.|
|StringOfObject_JML_Test.TestAddAll$1||Test for the addAll method.|
|StringOfObject_JML_Test.TestAddBeforeIndex||Test for the addBeforeIndex method.|
|StringOfObject_JML_Test.TestAddFront||Test for the addFront method.|
|StringOfObject_JML_Test.TestClone||Test for the clone method.|
|StringOfObject_JML_Test.TestComposedWith||Test for the composedWith method.|
|StringOfObject_JML_Test.TestConcat||Test for the concat method.|
|StringOfObject_JML_Test.TestElements||Test for the elements method.|
|StringOfObject_JML_Test.TestEquals||Test for the equals method.|
|StringOfObject_JML_Test.TestExt||Test for the ext method.|
|StringOfObject_JML_Test.TestExt$1||Test for the ext method.|
|StringOfObject_JML_Test.TestFrom||Test for the from method.|
|StringOfObject_JML_Test.TestFrom$1||Test for the from method.|
|StringOfObject_JML_Test.TestGet||Test for the get method.|
|StringOfObject_JML_Test.TestHas||Test for the has method.|
|StringOfObject_JML_Test.TestHashCode||Test for the hashCode method.|
|StringOfObject_JML_Test.TestInt_size||Test for the int_size method.|
|StringOfObject_JML_Test.TestIsEmpty||Test for the isEmpty method.|
|StringOfObject_JML_Test.TestIsPrefix||Test for the isPrefix method.|
|StringOfObject_JML_Test.TestIsProperPrefix||Test for the isProperPrefix method.|
|StringOfObject_JML_Test.TestIsProperSuffix||Test for the isProperSuffix method.|
|StringOfObject_JML_Test.TestIsSuffix||Test for the isSuffix method.|
|StringOfObject_JML_Test.TestIterator||Test for the iterator method.|
|StringOfObject_JML_Test.TestLength||Test for the length method.|
|StringOfObject_JML_Test.TestOccurs_ct||Test for the occurs_ct method.|
|StringOfObject_JML_Test.TestPow||Test for the pow method.|
|StringOfObject_JML_Test.TestProduct||Test for the product method.|
|StringOfObject_JML_Test.TestProductFrom||Test for the productFrom method.|
|StringOfObject_JML_Test.TestProductFromTo||Test for the productFromTo method.|
|StringOfObject_JML_Test.TestRev||Test for the rev method.|
|StringOfObject_JML_Test.TestReverse||Test for the reverse method.|
|StringOfObject_JML_Test.TestSingleton||Test for the singleton method.|
|StringOfObject_JML_Test.TestStringOfObject||Test for the StringOfObject contructor.|
|StringOfObject_JML_Test.TestStringOfObject$1||Test for the StringOfObject contructor.|
|StringOfObject_JML_Test.TestToString||Test for the toString method.|
|StringOfObject_JML_TestData||Supply test data for the JML and JUnit based testing of Person.|
|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.|
|UndefinedException||Exception used to indicate that a comparison is undefined.|
This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models. 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. This package also contains enumerators (which are mutable) for the types of immutable collections in the package.
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. Don'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.
The enumerator types 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 are described below.
Comparable interface, these interfaces
have a compareTo operation that can throw an
when the comparison between objects (of appropriate types) is undefined.
This allows the specification of partial orders.
On the other hand, the compareTo operation of the type
and its subtypes cannot throw this exception.
is essentially equivalent
See the package tree diagram (in the generated javadocs) for the details of the relationships among these interfaces.
Perhaps the most useful model types are the various kinds of
collections. (We use the term ``collection'' in a generic way,
since these types do not implement the
interface, because that assumes collections are mutable objects.)
The type NaturalNumber models infinite precision natural numbers.
The type StringOfObject models finite mathematical strings (i.e., sequences) of objects. The elements of a string are object references. When an object is inserted into such a string, it is not cloned. The equality test used by the has method uses Java's == operator to compare addresses of these objects.
The code relies heavily on the org.jmlspecs.models package, whenever possible.
In the test data classes (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 in collaboration with Stephen Edwards, Murali Sitaraman, and their students. The specifications are primarily based on the work of William Ogden, in particular his notes for CIS 680 at the Ohio State University.
This work was supported in part by the (US) National Science Foundation under grants CCR-0097907, and CCR-0113181.
|PREV PACKAGE NEXT PACKAGE||FRAMES NO FRAMES|