JML

Uses of Package
java.lang

Packages that use java.lang
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
Default Package  
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. 
Default Package  
org.multijava.relaxed.runtime   
org.multijava.relaxed.util   
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
Default Package  
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
           
 

Classes in java.lang used by Default Package
Appendable
           
Object
           
 

Classes in java.lang used by Default Package
Appendable
           
Object
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by Default Package
Object
           
String
           
 

Classes in java.lang used by Default Package
Appendable
           
CharSequence
           
ClassNotFoundException
           
Comparable
           
Exception
           
Object
           
Readable
           
SecurityManager
           
String
           
Throwable
           
 

Classes in java.lang used by Default Package
AbstractStringBuilder
           
Appendable
           
AssertionStatusDirectives
           
Byte
           
Character
           
CharSequence
           
Class
           
Class.EnclosingMethodInfo
           
ClassFormatError
           
ClassLoader
           
ClassNotFoundException
           
CloneNotSupportedException
           
Comparable
           
Double
           
Error
           
Exception
           
Float
           
IllegalAccessException
           
IllegalArgumentException
           
IndexOutOfBoundsException
           
InstantiationException
           
Integer
           
InterruptedException
           
Long
           
NoSuchFieldException
           
NoSuchMethodException
           
Number
           
NumberFormatException
           
Object
           
Package
           
RuntimeException
           
SecurityException
           
Short
           
StackTraceElement
           
String
           
StringBuffer
           
StringBuilder
           
Throwable
           
VirtualMachineError
           
 

Classes in java.lang used by Default Package
Class
           
Exception
           
IllegalAccessException
           
IllegalArgumentException
           
Object
           
SecurityException
           
String
           
Throwable
           
 

Classes in java.lang used by Default Package
ClassNotFoundException
           
Comparable
           
Number
           
Object
           
String
           
 

Classes in java.lang used by Default Package
ClassNotFoundException
           
Cloneable
           
CloneNotSupportedException
           
Exception
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by Default Package
CharSequence
           
ClassNotFoundException
           
Object
           
String
           
StringBuilder
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by Default Package
Object
           
 

Classes in java.lang used by org.jmlspecs.checker
ClassCastException
           
Cloneable
           
Comparable
           
Exception
           
Number
           
Object
           
Runnable
           
RuntimeException
           
String
           
Throwable
           
 

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

Classes in java.lang used by org.jmlspecs.jmldoc.jmldoc_142
Appendable
           
Comparable
           
Exception
           
Object
           
Runnable
           
String
           
StringBuffer
           
 

Classes in java.lang used by org.jmlspecs.jmlrac
Cloneable
           
Comparable
           
Exception
           
Object
           
Runnable
           
RuntimeException
           
String
           
StringBuffer
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.jmlrac.qexpr
Cloneable
           
Exception
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.jmlrac.runtime
Class
           
Error
           
Exception
           
NoSuchMethodException
           
Object
           
RuntimeException
           
SecurityException
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.jmlspec
Class
           
Cloneable
           
Comparable
           
Object
           
Runnable
           
String
           
 

Classes in java.lang used by org.jmlspecs.jmlunit
Comparable
           
Object
           
Runnable
           
String
           
StringBuffer
           
 

Classes in java.lang used by org.jmlspecs.jmlunit.strategies
Cloneable
           
Exception
           
InternalError
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.lang
Object
           
String
           
Throwable
           
 

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

Classes in java.lang used by org.jmlspecs.models
ArithmeticException
           
Byte
           
Character
           
ClassCastException
           
Cloneable
           
Comparable
           
Double
           
Exception
           
Float
           
IllegalArgumentException
           
IllegalStateException
           
IndexOutOfBoundsException
           
Integer
           
Long
           
NullPointerException
           
NumberFormatException
           
Object
           
RuntimeException
           
Short
           
String
           
Throwable
           
UnsupportedOperationException
           
 

Classes in java.lang used by org.jmlspecs.models.resolve
ClassCastException
           
Cloneable
           
Comparable
           
Exception
           
IllegalArgumentException
           
IndexOutOfBoundsException
           
NullPointerException
           
Number
           
Object
           
OutOfMemoryError
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.racwrap
Cloneable
           
Comparable
           
Object
           
String
           
 

Classes in java.lang used by org.jmlspecs.racwrap.runner
Class
           
ClassLoader
           
ClassNotFoundException
           
Exception
           
Object
           
String
           
 

Classes in java.lang used by org.jmlspecs.samples.dbc
Exception
           
IllegalArgumentException
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.digraph
Cloneable
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.dirobserver
Cloneable
           
Object
           
String
           
 

Classes in java.lang used by org.jmlspecs.samples.jmlkluwer
Cloneable
           
Exception
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.jmlrefman
Exception
           
IllegalArgumentException
           
NullPointerException
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.jmltutorial
Object
           
String
           
Throwable
           
 

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

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

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

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

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

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

Classes in java.lang used by org.jmlspecs.samples.misc
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.prelimdesign
Cloneable
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.reader
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.sets
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.stacks
CloneNotSupportedException
           
Exception
           
NullPointerException
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.samples.table
Cloneable
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.jmlspecs.util
Class
           
Object
           
String
           
 

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

Classes in java.lang used by org.multijava.dis
Double
           
Float
           
Long
           
Object
           
String
           
 

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

Classes in java.lang used by org.multijava.launcher
Object
           
Runnable
           
String
           
 

Classes in java.lang used by org.multijava.mjc
ArithmeticException
           
Character
           
Class
           
ClassCastException
           
ClassLoader
           
ClassNotFoundException
           
Cloneable
           
CloneNotSupportedException
           
Comparable
           
Double
           
Exception
           
Integer
           
Number
           
NumberFormatException
           
Object
           
Runnable
           
String
           
StringBuffer
           
Throwable
           
UnsupportedOperationException
           
 

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

Classes in java.lang used by Default Package
Appendable
           
Object
           
 

Classes in java.lang used by org.multijava.relaxed.runtime
Class
           
ClassLoader
           
ClassNotFoundException
           
Exception
           
IllegalAccessException
           
NoSuchMethodException
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by org.multijava.relaxed.util
Exception
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.multijava.util
Class
           
Cloneable
           
Comparable
           
Exception
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

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

Classes in java.lang used by org.multijava.util.classfile
ClassCastException
           
Comparable
           
Exception
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.multijava.util.compiler
Cloneable
           
Exception
           
Object
           
RuntimeException
           
String
           
Throwable
           
 

Classes in java.lang used by Default Package
Object
           
Runnable
           
 

Classes in java.lang used by org.multijava.util.guigen
Exception
           
Object
           
String
           
Throwable
           
 

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

Classes in java.lang used by org.multijava.util.lexgen
Exception
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.multijava.util.msggen
Exception
           
Object
           
String
           
Throwable
           
 

Classes in java.lang used by org.multijava.util.optgen
Exception
           
Object
           
String
           
Throwable
           
 

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

Classes in java.lang used by org.multijava.util.testing
Class
           
IllegalAccessException
           
IllegalArgumentException
           
Object
           
Process
           
String
           
 


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.