JML

JML Implementation Documentation

JML models
org.jmlspecs.lang This package is a collection of types used in the definition of the JML language.
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.

 

Java specs
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.security.interfaces  
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).

 

JML tools
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.launcher The launcher allows the user to access all of the tools in JML.
org.jmlspecs.racwrap  
org.jmlspecs.racwrap.runner  
org.jmlspecs.util  
org.jmlspecs.util.dis  

 

MultiJava tools
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.rmjc  
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.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.

 

JML samples
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 This package contains samples of JML specifications that are related to lists of various flavors.
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.list3  
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.

 

Other Packages
javax.crypto  
javax.servlet  
javax.servlet.http  
javax.xml.parsers  

 


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.