Uses of Package
java.lang

Packages that use java.lang

Default Package
Default Package
Default Package
java.awt
java.awt.color
java.awt.event
java.io	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.lang	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.lang.reflect	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.math	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.net	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.security	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.sql	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.util	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
java.util.regex	JML Specifications for the corresponding types in the Java Developement Kit (JDK).
javax.crypto
javax.servlet
javax.servlet.http
Default Package
Default Package
javax.xml.parsers
Default Package
Default Package
Default Package
Default Package
org.jmlspecs.ant.tasks
org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc	The jmldoc tool documents java programs that contain JML (Java Modeling Language) annotations included as specially formatted comments; the generated html pages are very similar to those produced by javadoc, but with annotation information added.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.
org.jmlspecs.jmlrac.runtime	Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc).
org.jmlspecs.jmlspec	A tool that can generate or compare specification skeletons from Java source or class files.
org.jmlspecs.jmlunit	Generates JUnit test classes from JML specifications.
org.jmlspecs.jmlunit.strategies	The types in this package are used in providing test data for JML/JUnit testing.
org.jmlspecs.lang	This package is a collection of types used in the definition of the JML language.
org.jmlspecs.launcher	The launcher allows the user to access all of the tools in JML.
org.jmlspecs.models	This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package.
org.jmlspecs.models.resolve	This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models.
org.jmlspecs.racwrap
org.jmlspecs.racwrap.runner
org.jmlspecs.samples.dbc	This package contains samples of JML specifications written in the style of design by contract.
org.jmlspecs.samples.digraph	This package contains samples of JML specifications for directed graphs.
org.jmlspecs.samples.dirobserver	This package contains samples of JML specifications that illustrate issues in component-based programming relating to callbacks and JML's model program feature.
org.jmlspecs.samples.jmlkluwer	This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design".
org.jmlspecs.samples.jmlrefman	This package contains samples of JML specifications from the JML Reference Manual.
org.jmlspecs.samples.jmltutorial	This package contains samples of JML specifications from the tutorials.
org.jmlspecs.samples.list.iterator
org.jmlspecs.samples.list.list1
org.jmlspecs.samples.list.list1.node
org.jmlspecs.samples.list.list2
org.jmlspecs.samples.list.node
org.jmlspecs.samples.list.node2
org.jmlspecs.samples.misc	This package contains miscellaneous samples of JML specifications.
org.jmlspecs.samples.prelimdesign	This package contains samples of JML specifications from the paper Preliminary Design of JML.
org.jmlspecs.samples.reader	This package contains samples of JML specifications relating to some abstractions of input and output.
org.jmlspecs.samples.sets	This package contains samples of JML specifications relating to sets.
org.jmlspecs.samples.stacks	This package contains samples of JML specifications relating to stacks of various sorts.
org.jmlspecs.samples.table	This package contains samples of JML specifications relating to tables.
org.jmlspecs.util
org.jmlspecs.util.dis
org.multijava.dis
org.multijava.javadoc
org.multijava.launcher	The launcher allows the user to access all of the tools in MJ.
org.multijava.mjc	Implements mjc, a MultiJava compiler.
org.multijava.mjdoc	The mjdoc tool documents java programs that contain MultiJava (MJ) extensions to the Java progamming language; it produces html pages very similar to those produced by the javadoc tool.
org.multijava.mjdoc.mjdoc_142	The mjdoc tool documents java programs that contain MultiJava (MJ) extensions to the Java progamming language; it produces html pages very similar to those produced by the javadoc tool.
org.multijava.relaxed.runtime
org.multijava.relaxed.util
org.multijava.universes.rt
org.multijava.util
org.multijava.util.backend	Provides an optimizer for methods for the compilers in MultiJava and the Java Modeling Language.
org.multijava.util.classfile	Provides an editor for classfiles used by MultiJava and the Java Modeling Language.
org.multijava.util.compiler	Provides utilities and superclasses for the compilers in MultiJava and the Java Modeling Language.
org.multijava.util.gui
org.multijava.util.guigen	Implements the automatic generation of all of the GUIs for MultiJava and the Java Modeling Language.
org.multijava.util.jperf	Defines the perfect hashing function generator Package Specification JPerf is the perfect hashing function generator for the compilers in MultiJava and the Java Modeling Language.
org.multijava.util.lexgen	Provides a lexer for the compilers of MultiJava and the Java Modeling Language.
org.multijava.util.msggen	Implements the automatic generation of the data structure for all of the compiler messages in MultiJava and the Java Modeling Language.
org.multijava.util.optgen	Implements the automatic generation of the data structure for all of the command line options in MultiJava and the Java Modeling Language.
org.multijava.util.optimize	Provides an optimizer for classfiles used by MultiJava and the Java Modeling Language.
org.multijava.util.testing	Provides JUnit testing utilities for all of the parts of MultiJava and the Java Modeling Language.

Classes in java.lang used by Default Package

Cloneable

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by java.awt

Object
JML's specification of java.lang.Object.

Classes in java.lang used by java.awt.color

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by java.awt.event

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by java.io

Class
JML's specification of java.lang.Class

ClassLoader

ClassNotFoundException

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

SecurityException

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Throwable

Classes in java.lang used by java.lang

AssertionStatusDirectives

Boolean
JML's specification of java.lang.Boolean.

Byte
JML's specification of java.lang.Byte.

Character
JML's specification of java.lang.Character.

Character.Subset

Character.UnicodeBlock

CharSequence
JML's specification of java.lang.CharSequence.

Class
JML's specification of java.lang.Class

ClassCastException

ClassFormatError

ClassLoader

ClassNotFoundException

CloneNotSupportedException

Comparable
JML's specification of java.lang.Comparable.

Double
JML's specification of java.lang.Double.

Error
JML's specification of java.lang.Error

Exception

Float
JML's specification of java.lang.Float.

IllegalAccessException

IllegalArgumentException

IndexOutOfBoundsException

InstantiationException

Integer
JML's specification of java.lang.Integer.

InterruptedException

Long
JML's specification of java.lang.Long.

NoSuchFieldException

NoSuchMethodException

Number
JML's specification of java.lang.Number.

NumberFormatException

Object
JML's specification of java.lang.Object.

Package
JML's specification of java.lang.Package

Process

Runnable
JML's specification of java.lang.Runnable.

Runtime

RuntimeException

SecurityException

SecurityManager
JML's specification of java.lang.SecurityManager

Short
JML's specification of java.lang.Short.

StackTraceElement
JML's specification of StackTraceElement.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

StringIndexOutOfBoundsException

Thread

ThreadGroup

ThreadLocal.ThreadLocalMap

Throwable

VirtualMachineError
JML's specification of java.lang.VirtualMachineError

Classes in java.lang used by java.lang.reflect

ArrayIndexOutOfBoundsException

Class
JML's specification of java.lang.Class

Exception

IllegalAccessException

IllegalArgumentException

InstantiationException

NegativeArraySizeException

Object
JML's specification of java.lang.Object.

SecurityException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by java.math

ClassNotFoundException

Comparable
JML's specification of java.lang.Comparable.

Number
JML's specification of java.lang.Number.

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by java.net

Class
JML's specification of java.lang.Class

ClassNotFoundException

Comparable
JML's specification of java.lang.Comparable.

Exception

IllegalAccessException

InstantiationException

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by java.security

Class
JML's specification of java.lang.Class

ClassLoader

Cloneable

CloneNotSupportedException

Exception

IllegalArgumentException

Object
JML's specification of java.lang.Object.

RuntimeException

SecurityException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by java.sql

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by java.util

ClassLoader

ClassNotFoundException

Cloneable

CloneNotSupportedException

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by java.util.regex

CharSequence
JML's specification of java.lang.CharSequence.

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Classes in java.lang used by javax.crypto

Class
JML's specification of java.lang.Class

Exception

IllegalStateException

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by javax.servlet

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by javax.servlet.http

Cloneable

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by javax.xml.parsers

Error
JML's specification of java.lang.Error

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by Default Package

Object
JML's specification of java.lang.Object.

Classes in java.lang used by org.jmlspecs.ant.tasks

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.checker

ClassCastException

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Exception

Number
JML's specification of java.lang.Number.

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.jmldoc

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.jmldoc.jmldoc_142

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Classes in java.lang used by org.jmlspecs.jmlrac

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

RuntimeException

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Throwable

Classes in java.lang used by org.jmlspecs.jmlrac.qexpr

Cloneable

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.jmlrac.runtime

Class
JML's specification of java.lang.Class

Error
JML's specification of java.lang.Error

Exception

NoSuchMethodException

Object
JML's specification of java.lang.Object.

RuntimeException

SecurityException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.jmlspec

Class
JML's specification of java.lang.Class

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.jmlunit

Comparable
JML's specification of java.lang.Comparable.

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Classes in java.lang used by org.jmlspecs.jmlunit.strategies

Cloneable

Exception

InternalError
JML's specification of java.lang.InternalError

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.lang

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.launcher

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.models

ArithmeticException

Byte
JML's specification of java.lang.Byte.

Character
JML's specification of java.lang.Character.

ClassCastException

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Double
JML's specification of java.lang.Double.

Exception

Float
JML's specification of java.lang.Float.

IllegalArgumentException

IllegalStateException

IndexOutOfBoundsException

Integer
JML's specification of java.lang.Integer.

Long
JML's specification of java.lang.Long.

NullPointerException

NumberFormatException

Object
JML's specification of java.lang.Object.

RuntimeException

Short
JML's specification of java.lang.Short.

String
JML's specification of java.lang.String.

Throwable

UnsupportedOperationException

Classes in java.lang used by org.jmlspecs.models.resolve

ClassCastException

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Exception

IllegalArgumentException

IndexOutOfBoundsException

NullPointerException

Number
JML's specification of java.lang.Number.

Object
JML's specification of java.lang.Object.

OutOfMemoryError

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.racwrap

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.racwrap.runner

Class
JML's specification of java.lang.Class

ClassLoader

ClassNotFoundException

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.dbc

Exception

IllegalArgumentException

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.digraph

Cloneable

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.dirobserver

Cloneable

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.jmlkluwer

Cloneable

Exception

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.samples.jmlrefman

Exception

IllegalArgumentException

NullPointerException

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.jmltutorial

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.list.iterator

Object
JML's specification of java.lang.Object.

Classes in java.lang used by org.jmlspecs.samples.list.list1

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.list.list1.node

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.list.list2

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.list.node

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.list.node2

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.misc

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.prelimdesign

Cloneable

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.reader

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.sets

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.samples.stacks

CloneNotSupportedException

Exception

NullPointerException

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.jmlspecs.samples.table

Cloneable

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.util

Class
JML's specification of java.lang.Class

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.jmlspecs.util.dis

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.dis

Double
JML's specification of java.lang.Double.

Float
JML's specification of java.lang.Float.

Long
JML's specification of java.lang.Long.

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.javadoc

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.launcher

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.mjc

ArithmeticException

Character
JML's specification of java.lang.Character.

Class
JML's specification of java.lang.Class

ClassCastException

ClassLoader

Cloneable

CloneNotSupportedException

Comparable
JML's specification of java.lang.Comparable.

Double
JML's specification of java.lang.Double.

Exception

Integer
JML's specification of java.lang.Integer.

Number
JML's specification of java.lang.Number.

NumberFormatException

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

StringBuffer
JML's specification of StringBuffer.

Throwable

UnsupportedOperationException

Classes in java.lang used by org.multijava.mjdoc

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.mjdoc.mjdoc_142

Exception

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.relaxed.runtime

Class
JML's specification of java.lang.Class

ClassLoader

ClassNotFoundException

Exception

IllegalAccessException

NoSuchMethodException

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.relaxed.util

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.universes.rt

Object
JML's specification of java.lang.Object.

Classes in java.lang used by org.multijava.util

Class
JML's specification of java.lang.Class

Cloneable

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.backend

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.util.classfile

ClassCastException

Comparable
JML's specification of java.lang.Comparable.

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.compiler

Cloneable

Exception

Object
JML's specification of java.lang.Object.

RuntimeException

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.gui

Object
JML's specification of java.lang.Object.

Runnable
JML's specification of java.lang.Runnable.

Classes in java.lang used by org.multijava.util.guigen

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.jperf

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.util.lexgen

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.msggen

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.optgen

Exception

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Throwable

Classes in java.lang used by org.multijava.util.optimize

Object
JML's specification of java.lang.Object.

String
JML's specification of java.lang.String.

Classes in java.lang used by org.multijava.util.testing

Object
JML's specification of java.lang.Object.

Process

String
JML's specification of java.lang.String.