jmldoc - The JML documentation tool

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.

Rationale

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.

Architecture

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:

org.jmlspecs.jmldoc - the jmldoc Main class and adaptor classes
org.jmlspecs.checker - the JML checker
org.multijava.mjdoc - the mjdoc Main class and adaptor classes
org.multijava.mjc, org.multijava.util and its subpackages - the multijava compiler
the antlr (2.7.2) runtime library
the gnuopt command-line option parsing library
the libraries for the javadoc tool and the doclet API. These are either part of your java installation or in an archive named tools.jar. If the command javap com.sun.tools.doclets.standard.Standard successfully lists the API for the Standard class, then your CLASSPATH contains the appropriate reference.

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.

Class-level annotations such as invariants are added into a block of html in the generated html file for the class, in a format similar to the class field and class methods summary display. Separate sections also show any class-level specifications inherited from super classes and interfaces. The latter are shown only if the annotated source code of the super classes and interfaces is available at the time the documentation files are being generated.
Method-level annotations, such as preconditions and postconditions, are added to the commentary about a method given in the "Method Detail" section of the generated documentation. The specifications of overridden methods are also included whenever the source code for the overridden methods is available at the time the documentation is being generated.
Constructor-level annotations are added to the commentary in the "Constructor Detail" section of the generated html page.
The formal arguments of methods and constructors (in the Detail section) are shown with a 'non_null' modifier if they have been so annotated.
Field-level annotations are added to the commentary about a field in the "Field Detail" section of the generated documentation.
Additional "Model Field Summary", "Ghost Field Summary", "Model Field Detail", and "Ghost Field Detail" sections, analogous to the sections about Fields are added to the documentation in order to document model and ghost fields declared in the annotations. Model and ghost fields inherited from super classes and interfaces are also referenced.
jmldoc includes the functionality of mjdoc and will generate documentation appropriate to MultiJava if the source code contains MultiJava extensions, as described in the documentation of the mjdoc tool.

Documentation

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.

The syntax of javadoc tags and the available javadoc command-line options are described at the javadoc web page.
The syntax of JML annotations is described in the Preliminary Design Document.

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.

-author : causes information in @author tags to be put into the html pages; the default is to omit the information
-bootclasspath classpath : specifies the set of directories and jar files in which the Java system classes are found; the default is system specific.
-bottom string : a string of HTML content to be placed at the end of the file, below the lower navigation bar
-breakiterator : in javadoc controls the algorithm that determines the summary sentence of a comment; the option is ignored in jmldoc since jmldoc always behaves like javadoc with -breakiterator enabled.
-charset string : specifies the HTML character set for the document as given in the usual META tag; the default is to omit the META html tag.
-classpath pathlist : the set of root locations (directories and jar files) in which jmldoc will look for class files for all referenced classes (those not on the command-line but referenced by files and packages on the command-line). The default is the value of the environment variable CLASSPATH, or the current directory if CLASSPATH is not defined. This option is equivalent to --classpath and -C.
-d directorypath : specifies the root location for the generated html files (relative to the current directory). The default is the current directory. javadoc 1.3 does not create the directory if it does not exist; jmldoc and javadoc 1.4 will create the directory. (Equivalent to --destination.)
-docencoding name : specifies the html encoding for generated files; the default is the default encoding of the local java virtual machine
-docfilessubdirs : recursively copy doc-file subdirectories
-doclet class : uses the given (fully-qualified) class as the doclet class to use instead of the MjdocStandard class. See the doclet API for more information about writing new doclets.
-docletpath classpathlist : specifies a path to or jar file containing the doclet specified in the -doclet option. The default is the value of -classpath (NOT IMPLEMENTED - add the doclet location to the classpath instead).
-doctitle string : uses the given string as the displayed title in the generated overview html page; the default is no title.
-encoding name : specifies the encoding name of the source files, otherwise uses a platform-specific default
-exclude pkglist : specifies a list of packages to exclude from being documented
-excludedocfilessubdir name1:name2:... : exclude any listed doc-files subdirectories
-extdirs directorylist : specifies the directories where extension classes are found (NOT IMPLEMENTED - use bootclasspath instead)
-footer string : a string of HTML content to be placed to the right of the lower navigation bar; the default for the footer is the header string
-group groupheading packagepatternlist : allows the organization of the packages listed on the overview page into specified groups, as described in the javadoc documentation; by default all the packages are in one group.
-header string : a string of HTML content to be placed to the right of the upper navigation bar
-help : prints out a usage message and terminates (equivalent to --help)
-helpfile filepath : specifies the file that contains the description of how to use the generated html pages. A copy of this file is made and stored in the top-level directory of the documentation set (using the given filename), and linked to by the HELP link in the documentation pages. Without this option, jmldoc (like javadoc) generates its own file at a hard-coded filename. The specified path to the filename is either an absolute path or a path relative to the current directory.
-Jflag : specifies runtime system options
-link url : specifies a url (either http: or file:) at which to find the html documentation of classes that are referenced in the classes being documented but whose documentation is not itself being generated in this run of jmldoc. It is allowed to have multiple -link options. It is required that there be a file named package-list at the specified url; this file contains the list of packages that are documented at that location.
-linkoffline url url-or-directory : as for the -link option, this specifies the location of html files for classes not being documented in the current jmldoc run. In this case the url-or-directory gives the location of the package-list file that contains a list of packages that are documented at the location url. The url need not be available at the time the documentation is generated, though of course, it will have to be available when the link is activated in the produced documentation.
-linksource : generate links to html files containing source code
-locale locale-name : specifies the locale to be used for rendering text (place this option first) (NOT IMPLEMENTED in jmldoc)
-nocomment : suppress description and tags, generating only declarations
-nodeprecated : prevents the generation of any documentation of deprecated elements (as well as doing what -nodeprecatedlist does)
-nodeprecatedlist : prevents the generation of the deprecated-list.html file, which contains a list of deprecated elements
-nohelp : omits the generation of a help file (how to use the generated html pages)
-noindex : prevents the generation of an index as part of the documentation
-nonavbar : omits the header, footer and navigation bars
-nooverview : prevents an overview file from being created when more than one package is being documented
-noqualifier name1:name2:... : exclude the list of qualifiers from the output
-nosince : prevents the listing of any information from @since tags
-notree : omits the class/interface tree from the generated documentation
-overview path/filename : causes jmldoc to create an overview page using the information in the given overview file; the given path/filename must be an html file. If it is a relative path, it must exist relative to one of the directories in the given -sourcepath (the first such file that exists is used). In jmldoc, an overview file is created by default if more than one package is being documented. Typically -sourcepath refers to the root directory of the packages being implemented, path/ is omitted, and filename is overview.html. (Despite the javadoc documentation, javadoc 1.3 looks for the specified overview file relative to the current directory.)
-privacy : This is a jmldoc-only selectable collection if the public/protected/package/private options (see below). Rather than using the functions below, specify an integer for the level of class members documented on the html pages. Specify 0 for public, 1 for protected, 2 for package, and 3 for private. The default is 1 (-protected).
-public, -protected, -package, -private : These control which classes and class members are documented on the html pages, according to their declared access level. The default is -protected.
-quiet: Turns off any informational messages from the javadoc doclet api (Now equivalent to --Quiet)
-serialwarn : causes warnings to be generated for missing @serial tags (NOT IMPLEMENTED)
-source release : provide source compatibility with specified release
-sourcepath pathlist : the set of root locations to search for the packages specified on the command-line. The default is the value of -classpath.
-splitindex : if an index is generated, generates it as a number of smaller files instead of one large file
-subpackages subpkglist : specifies subpackages to recursively load
-stylesheetfile filepath : specifies a file to use as the HTML stylesheet file; it is copied to the root directory of the documentation set (retaining the same filename); the default behavior is simply to write a standard default css file using the filename stylesheet.css. The specified path to the filename is either an absolute path or a path relative to the current directory.
-tag name:location:header : specifies a single argument custom tag
-taglet name : specifies a fully-qualified name of a taglet class
-tagletpath pathlist : the pathlist in which to find taglet classes
-use : adds the use information pages (one per class and package) to the generated documentation
-verbose : not applicable to jmldoc (causes printing of timing details of parsing in javadoc)
-version : cause information in @version tags to be put into the html pages
-windowtitle string : uses the given string in the TITLE tag of the generated html pages (so that it appears in the title bar and bookmarks or favorites lists of the browser). The javadoc documentation says that the default is the value of -doctitle; however javadoc (and jmldoc) actually produces a title of "Generated Documentation (Untitled)" on the frame-style overview page and an empty prefix on other pages.
-x : prints out a list of special (javadoc) options
-xnodate : a special option that causes html pages to have the string 'TODAY' instead of a current date and time

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.

--Quiet, -Q : shuts off any jmldoc informational messages, including the effect of --quiet; this is now equivalent to -quiet
--classpath classpath, -C classpath : specifies the root directories where referenced classes and packages are found; equivalent to -classpath
--deprecation : not applicable to jmldoc (in mjc it prevents deprecated methods from being called); use -nodeprecated above to avoid listing deprecated classes and methods in the generated documentation
--destination directory, -d directory : equivalent to the -d javadoc option; it causes all output files to be created relative to the given directory; the default is the current directory.
--docpath directorylist : pathlist in which to find javadoc files (provides functionality similar to -link, but all in one pathlist in one option)
--help, -h : simply prints out usage information and terminates, without processing any files (equivalent to -help)
--norecursive : disables the -recursive option (the default is non-recursive)
--recursive, -R : causes jmldoc to document java and jml files in any subdirectories (and sub-subdirectories, etc., recursively) of directories listed on the command-line. See also the -subpackage option in javadoc 1.4 for a slightly different but similar functionality.
--showPromotion, -U : show both implicit and explicit promotions (widening coercions) in rendered annotations; if false (the default), neither are shown.
--sourcepath directorylist, -S directorylist : equivalent to -sourcepath above
--version, -V : displays the version number of the jmldoc program and terminates
--warning int, -w int : controls the pickiness of the warnings produced by jmldoc, in an undocumented way

These options apply to the MultiJava enhancements, as described for the mjdoc tool:

--fcns arg : specifies which generic function html pages should be produced. If arg is none, no generic function pages are produced; if arg is ext (the default), then pages are produced only for external methods; if arg is all, then pages are produced for both internal and external methods. [ -all is experimental and incomplete ]
--multijava, -M : enables multijava extensions (default is enabled)
--nomultijava : disables multijava extensions

These jmldoc options are used mostly for debugging:

--debug, -c : enables the production of copious debugging information
--filter qualifiedName, -f qualifiedName : names a filter to filter error and warning messages
--keepGoing, -k : instructs jmldoc to continue on after reporting errors, even at the risk of runtime exceptions
--quiet, -q : enables the printing of timing information about each compilation phase
--verbose, -v : enables the printing of tracing information about each compilation phase

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.

If the argument is an absolute or relative (relative to the current working directory) path to a readable file, it is considered a filename.
Otherwise, if the argument is a syntactically valid package name (java identifier or a sequence of java identifiers separated by '.' characters), it is considered a package name (whether or not it exists).
Otherwise, if the argument is an absolute or relative (relative to the current working directory) path to an existing directory, it is considered a directory. (A simple name can be interpreted as a directory by writing it as ./dir).
Otherwise, the command-line argument is invalid.

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.

The warnings generated by javadoc are not documented; the set of warnings generated by jmldoc is different, and the warning messages may have a different format.
The resolution of class names specified in @see, @link, or @throws tags is somewhat different between the two tools. There may be some links or warnings about links that are generated with one tool that are not generated with the other.
The jmldoc tool removes some blank lines that would appear in javadoc output.
The output of javadoc contains an html comment in the generated files that says "Generated by javadoc"; jmldoc replaces that with "Generated by jmldoc"
The algorithm for determining the summary (first) sentence of a javadoc comment may differ.
The javadoc documentation says that the file specified by the -overview option is looked for relative to the directories on the given sourcepath, or relative to the current directory if no sourcepath is given. This behavior is implemented in jmldoc, but javadoc actually only looks relative to the current directory.

Bugs and features not yet implemented

The -docletpath option is not implemented.
The -extdirs option is not implemented.
The -locale option is not implemented.
The -subpackages option is not implemented.
The -exclude option is not implemented.
The -docfilessubdirs and -excludedocfilessubdir options are not implemented.
The resolution of class names in tags must be corrected.
The type names of parameters of methods in see and link tags must be fully qualified
Some of the non-javadoc text rendered by jmldoc is only in English and not affected by the -locale option
Constructs that are MultiJava extensions, such as the two parts of a MultiJava specialized type, may not be represented in the use or index pages.
The FRAMES/NO FRAMES options on a generic function html page do not work correctly.
Some html files generated by jmldoc still have comments saying they are generated by javadoc.
Anything to do with serial/serializable tags is not 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:

Description needed ???

Acknowledgements

The implementation of jmldoc has relied upon many contributions:

the implementation of the multijava compiler, provided by the MJC project, courtesy of and with thanks to those who have contributed to its development (see the MultiJava home page for a current list of contributors);
the previous version of jmldoc and jml and their contributors;
the concept and design of the first version of jmldoc as described in this paper: Arun D. Raghavan. Design of a JML documentation generator. Department of Computer Science, Iowa State University, TR #00-12, March 2000 [abstract] [postscript];
the advice, assistance and encouragement of individuals currently active in the MJC and JML projects, particularly Gary Leavens, Curtis Clifton, and Todd Milstein;
the documentation of javadoc and the documentation and implementation of the Standard Doclet as provided by Sun MicroSystems, about which Sun writes "One reason to look at the standard doclet is that it serves as a good example of the use of much of the doclet API. A second reason is that by seeing how the standard doclet produces the default HTML output, it will be easier for you to modify the standard doclet to make your own doclet for generating custom API documentation." and "If you want HTML output with roughly the same format as the default output, you can use the standard doclet as a starting point for creating your doclet. You can subclass appropriate classes in the standard doclet and then add or override methods as necessary to produce the output you want. Or you can copy the whole standard doclet and modify it.";
David Cok, who has been (as of May 2002) the principal author of mjdoc and the current version of jmldoc.