Package 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.


Class Summary
JavadocOptions This class is automatically generated from JavadocOptions.opt and contains member fields corresponding to command-line options.
JmldocGUI This class just has a main routine that invokes the main routine in the subpackage appropriate to the version of the Java tools library that is on the classpath.
JmldocOptions This class is automatically generated from JmldocOptions.opt and contains member fields corresponding to command-line options.
Main This class just has a main routine that invokes the main routine in the subpackage appropriate to the version of the Java tools library that is on the classpath.
Utils This class simply contains some utility methods

Package org.jmlspecs.jmldoc Description

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. It also recognizes and documents MultiJava (MJ) extensions to the Java progamming language.

The tool is provided as part of and in association with the other JML tools (and on the same licensing terms). It is provided for the purpose of research and education in the area of documentation, specification and verification of programs, particularly with respect to Java and to JML.

Questions and bug reports can be sent via the sourceforge trackers for JML.


The javadoc tool is useful in providing web-based html documentation for java programs and libraries. It allows documentation to be maintained in the same source files as the program code, which helps the software developers keep the source code consistent with the documentation and specifications. But the tool enables the documentation to be formatted in a useful html format that is easily browsed, with relevant links for cross-references.

The JML project has defined machine-readable annotations that assist in specifying and checking the intended behavior of Java classes and methods. These appear as comments to Java and so are ignored by Java. The jmldoc tool renders these annotations as additional html content that is added to the conventional javadoc-produced pages. Since jmldoc is built from mjdoc (the documentation tool for the MultiJava compiler), it also parses and documents the extensions to Java provided by the MultiJava project. More information on those extensions is available in the documentation of the mjdoc tool.


The jmldoc tool uses the language parser of the multijava compiler project. The doclet extension mechanism of the javadoc API is used to render the html documentation pages. Ordinarily, java doclets use the javadoc services to parse java source files, producing a parse tree of relevant material. This tree is passed to either the standard doclet to be rendered to standard javadoc html pages or to a user-supplied doclet to achieve some user-defined purpose. In the case of jmldoc, appropriate adaptor classes take the parse trees from the multijava parser, wrap them in objects implementing the interfaces of the doclet API, and pass the resulting parse tree to a slight modification of the standard doclet. The slight modifications preserve all the usual html generated for javadoc pages, but add functionality appropriate to the multijava extensions.

The current version of this tool uses javadoc 1.4. It will not compile or run with the doclet library from earlier versions of java.

Previous work and references

Though the code base is completely new, and now utilizes the doclet api for javadoc, the the initial design of the javadoc tool for JML (jmldoc) was created by Arun D. Raghavan, as described in "Design of a JML documentation generator" (Iowa State University, Dept. of Computer Science, TR00-12, March 2000). [abstract] [postscript]

Running the jmldoc tool

In order to run the jmldoc tool, you must have on your CLASSPATH: All of these, except the doclet jar, are available together in the JML release.

With the CLASSPATH appropriately set (it must include the paths to packages you wish to document), execute

java org.jmlspecs.jmldoc.Main options files packages

with command-line options and arguments as described below (the options, files, and packages may be intermixed and may appear in any order).

Alternatively, one can be specific about classpaths and write

java -classpath cp1 org.jmlspecs.jmldoc.Main -classpath cp2 -sourcepath cp3 ...

where cp1 is a classpath containing paths to the packages listed above (and defaults to the environment setting of CLASSPATH), and cp2 is a classpath containing paths to find .class files for classes referenced by parsed files (defaults to cp1), and cp3 is a classpath used for finding packages listed on the command-line (defaults to cp2). The files and directories on the command-line are looked for in the current working directory. Packages on the command-line are looked for in the directories that make up the sourcepath. Note that, just as with javadoc, the source files must be available in order to generate documentation files with javadoc comments reflected in them.

Enhancements provided by jmldoc

The output of jmldoc contains the following enhancements over javadoc.


The jmldoc tool is intended as a drop-in replacement for javadoc. That is, it accepts source files with all the tags accepted by javadoc, and it accepts all the command-line options that are accepted by javadoc. If presented with conventional java files and only javadoc command-line options, it produces the same output as javadoc. (Any differences in implementation are noted below). There are additional command-line options defined by jmldoc, described below.

Command-line options

The following are the command-line options available for javadoc 1.4 using the default (standard) doclet; they are also accepted by jmldoc. These options begin with a single hyphen and may not be abbreviated. The effect of these options is described more completely in the Javadoc 1.4 documentation. The following descriptions are summaries from the javadoc documentation. Javadoc option names (but not the arguments of the options, nor the jmldoc-specific options) are case-insensitive.

The following are additional options available in jmldoc. These options have a long form, which begin with a double hyphen, and a short form, which consist of a single hyphen and a single letter. If a short form option has a single argument, it may be concatenated with the hyphen and letter or it may be separated from them by white space.

These options apply to the MultiJava enhancements, as described for the mjdoc tool: These jmldoc options are used mostly for debugging:

Treatment of files, packages and directories listed on the command line

In addition to the command-line options and their arguments described above, the command-line for jmldoc may contain filenames, directories and package names. A command-line argument that is not an option or option argument is interpreted as follows.

A command-line argument that is considered a filename must be the name of a valid JML input file (i.e. a .java, .jml, .spec, .java-refined, .jml-refined, .spec-refined, .refines-java, .refines-jml, .refines-spec file), and it must contain valid multijava source code (i.e. compiled without error by mjc and checked without error by the jml checker). Relative pathnames are relative to the current working directory (regardless of the values of the CLASSPATH environment variable or the classpath or sourcepath command-line options).

If the argument denotes a package, then it is expected to be a valid package name rooted at a directory listed in the sourcepath. Specifying a collection of files to the jmldoc application as a package rather than as individual files causes jmldoc to generate additional package-level and overview level documentation, as described in the javadoc documentation.

If the argument is a directory, then jmldoc processes all JML input files with active suffixes in the given directory. If the -R (or --recursive) option has been specified, then all JML input files in any subdirectory (and, recursively, sub-subdirectories, etc.) are also processed just like directories specified on the command-line are processed.

Differences from javadoc

The jmldoc tool extends javadoc, as described above. On strict java files with only javadoc command-line arguments, jmldoc output differs slightly from javadoc output in the following ways.

Bugs and features not yet implemented

Differences from the doclet API

The jmldoc code contains an implementation of the Doclet API, as specified by Sun MicroSystems. There is also an implementation of that API implicit in the implementation of the javadoc application, and used by the Standard Doclet and other doclets. There are some known differences between the jmldoc and Standard doclet implementations, beyond the extensions needed for JML or MultiJava:


The implementation of jmldoc has relied upon many contributions:


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.