|
JML | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||
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 | |
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.
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.
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 | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||