JML

Package java.lang

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

See:
          Description

Interface Summary
Appendable  
CharSequence  
Cloneable  
Comparable  
Readable  
Runnable  
 

Class Summary
AbstractStringBuilder  
AssertionStatusDirectives  
Byte  
Character  
Class  
Class.EnclosingMethodInfo  
ClassLoader  
Double  
Float  
Integer  
Long  
Math  
Number  
Object  
Package  
Process  
SecurityManager  
Short  
StackTraceElement  
String  
StringBuffer  
StringBuilder  
Throwable  
 

Exception Summary
ArithmeticException  
ClassCastException  
ClassNotFoundException  
CloneNotSupportedException  
Exception  
IllegalAccessException  
IllegalArgumentException  
IllegalStateException  
IndexOutOfBoundsException  
InstantiationException  
InterruptedException  
NoSuchFieldException  
NoSuchMethodException  
NullPointerException  
NumberFormatException  
RuntimeException  
SecurityException  
UnsupportedOperationException  
 

Error Summary
ClassFormatError  
Error  
InternalError  
LinkageError  
OutOfMemoryError  
VirtualMachineError  
 

Package java.lang 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. Many of these were specified by Gary T. Leavens and Brandon Shilling, and David Cok has contributed several specifications as well. They have been refined by David R. Cok, using JML's connection to JUnit, along with 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.