JML

Package java.util

JML Specifications for the corresponding types in the Java Developement Kit (JDK).

See:
          Description

Interface Summary
Collection JML's specification of java.util.Collection.
Comparator  
Enumeration JML's specification of java.util.Enumeration.
EventListener  
Iterator JML's specification of java.util.Iterator.
List JML's specification of java.util.List.
ListIterator JML's specification of java.util.Iterator.
Map JML's specification of java.util.Map.
Map.Entry  
Observer JML's specification of the java.util.Observer.
RandomAccess  
Set JML's specification of java.util.Set.
SortedMap JML's specification of java.util.SortedMap.
SortedSet JML's specification of java.util.SortedSet.
 

Class Summary
AbstractCollection  
AbstractList JML's specification of java.util.AbstractList.
AbstractMap  
AbstractMap.SimpleEntry  
AbstractSequentialList  
AbstractSet JML's specification of java.util.AbstractSet.
ArrayList JML's specification of ArrayList.
Arrays JML's specification of java.util.Arrays.
BitSet JML's specification of the java.util.BitSet.
Calendar JML's specification of java.util.Calendar.
Date JML's specification of java.util.Date.
Dictionary  
EventObject  
GregorianCalendar JML's specification of java.util.Calendar.
HashMap JML's specification of java.util.HashMap.
HashMap.Entry  
HashSet JML's specification of java.util.HashSet.
Hashtable JML's specification of java.util.Hashtable.
LinkedHashSet  
LinkedList JML's specification of java.util.LinkedList.
Locale  
Observable JML's specification of the java.util.Observable.
Properties  
Random  
RandomAccessSubList  
ResourceBundle  
Stack JML's specification of Stack.
SubList  
TimeZone  
TreeMap JML's specification of java.util.TreeMap.
TreeMap.Entry  
TreeSet JML's specification of java.util.TreeSet.
Vector JML's specification of java.util.Vector.
 

Exception Summary
MissingResourceException  
NoSuchElementException  
 

Package java.util Description

JML Specifications for the corresponding types in the Java Developement Kit (JDK). These specifications are intended for use in reasoning about specifications in the JDK, but are not endorsed by Sun Microsystems, Inc. in any way. The syntactic interfaces of the methods are copyright Sun Microsystems, Inc.

Specification Conventions

Specifications in .spec files should be interfaces, and these are compiled with JML's runtime assertion checking compiler (jmlc) to yield surrogate class files that are in the release. Other specifications should normally be found in .jml or .refines-spec files.

The specifications necessarily start with the Java interfaces, but we never include the javadoc comments or code from the JDK, since that would violate copyright restrictions.

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 Sun Microsystems. They were specified by Gary T. Leavens, Brandon Shilling, Katie Becker, Kristina Boysen, Curtis Clifton, Clyde Ruby, and David R. Cok. They have been refined by David R. Cok, with help from JML users. The specification of Object, and the enumerators, iterators, and collections in the JDK 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.


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.