JML

Package org.jmlspecs.models.resolve

This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models.

See:
          Description

Interface Summary
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 UndefinedException and only throws a ClassCastException when the class of the argument prohibits comparison.
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.
 

Class Summary
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.
TestSuite.TestSuite$1  
 

Exception Summary
UndefinedException Exception used to indicate that a comparison is undefined.
 

Package org.jmlspecs.models.resolve Description

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.

Overview

There are several kinds of types in this package. These are described below.

Kinds of CompareTo

The interface CompareTo and its subtypes (such as AntisymmetricCompareTo, PreorderedCompareTo, etc.) represent different assumptions about a type's compareTo operator.

Unlike the Comparable interface, these interfaces have a compareTo operation that can throw an UndefinedException 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 TotalCompareTo and its subtypes cannot throw this exception.

The type TotallyOrderedCompareTo is essentially equivalent to Comparable.

See the package tree diagram (in the generated javadocs) for the details of the relationships among these interfaces.

Collections

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 Collection interface, because that assumes collections are mutable objects.)

Primitive types

The type NaturalNumber models infinite precision natural numbers.

Object collections

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.

Coding

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.

Acknowledgments

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.