The JMLdoc tool

javadoc with JML specifications
David R. Cok - June 2009

JMLdoc tool for generating Javadoc with JML specifications

The jmldoc tool adds JML specifications to the usual javadoc documentation. The source for that tool is contained in the org.jmlspecs.openjml.jmldoc package. The use and design of the tool are described here.

The javadoc tool provides HTML pages that conveniently summarize the API and documentation provided by a set of source code. The jmldoc tool is an enhancement of javadoc that adds to the javadoc documentation the JML specifications that are present in the source code. The jmldoc tool is a drop-in replacement for javadoc, with additional functionality and additional options.

The tool also enhances the javadoc information by including any Java programming language annotations associated with a type, method, or field in the summary of that program element.

Installation

The jmldoc tool is provided as a zip containing these files:

Use

License

The JML extensions to the OpenJDK version of javadoc are (c) 2009 by David R. Cok. OpenJDK is licensed using the GPLv2. You can find out more about OpenJDK at the OpenJDK website. Jmldoc is derived from OpenJDK and thus the GPLv2 applies to it also. The sourcecode for jmldoc is available at the OpenJML subproject of the JML project at sourceforge.net.

Known Bugs

The following are known issues with the jmldoc output.

Design Description

OpenJML

The jmldoc tool is an extension of the OpenJDK source code. Consequently it parses Java 1.6 code and handles Java 1.7 in so far as it is implemented in OpenJDK (as of this writing jmldoc is built on build ???FIXME of OpenJDK).

In so far as possible, jmldoc is a pure extension of the javadoc tool in OpenJDK. Some changes to the code of javadoc were required: some visibility modifiers were changed to protected or public where the modified elements were needed in derived classes. MORE????

Current design

The jmldoc tool has to combine functionality from two sources: the openjml tool to parse the specifications associated with Java program elements and the javadoc tool to output the desired HTML pages. These two tools enter program elements into symbol tables differently (openjml uses the techniques supplied by the OpenJDK Java compiler); it would require a maintenance-intensive merging of the two implementations into a third one to use these tools directly. Instead, jmldoc uses the OpenJDK facility of independent, co-existing compilation contexts. The Java code is parsed and represented using javadoc, then parsed and separately represented using openjml, and then, information from the openjml JML specifications is added into the javadoc HTML pages as those HTML pages are generated. This approach has only a few minor drawbacks: the code is parsed twice; symbol table entries from one compilation context have to be translated into the other context; and the Javadoc Doc structure does not actually contain JML elements such as model fields, methods, and classes.

The Main class that contains the entry points for the jmldoc tool could, corresponding to the discussion above, derive from either the Main class of openjml or the Main class of javadoc. Since openjml requires more tool initialization, it was more convenient to derive jmldoc's Main from openjml's. Command-line options that jmldoc adds to javadoc are processed in Main and help information is provided by the JmlStart class.

In order to generate JML information in the HTML output, the current jmldoc implementation extends the javadoc source code as follows. Javadoc operates by executing a set of Writers for various program elements. These have interfaces (e.g. ClassWriter) and specific implementations (e.g. ClassWriterImpl). In order to reuse as much code as possible so that the maintenance of jmldoc as javadoc evolves is minimized, the jmldoc tool implemented its own set of writers (e.g. ClassWriterJml) that extend the corresponding javadoc writers. Thus the classes ClassWriterJml, FieldWriterJml, MethodWriterJml, ConstructorWriterJml, and NestedClassWriterJml were created.

Javadoc instantiates these writers using a writer factory, WriterFactoryImpl, which is an implementation of the interface WriterFactory. In order to have the various JML writers instantiated at the correct time, jmldoc has its own implementation of WriterFactory, namely, WriterFactoryJml. The WriterFactoryImpl class is not written to be extended, so WriterFactoryJml is a direct implementation of WriterFactory, at the cost of duplicating code from WriterFactoryImpl.

Javadoc instantiates the WriterFactory in a Configuration object. Javadoc's implementation of Configuration (an abstract class) is ConfigurationImpl. Jmldoc extends ConfigurationImpl as ConfigurationJml in order to instantiate a WriterFactoryJml instead of a WriterFactoryImpl. This class also supplies a version string giving the date of the build represented by the tool.

The Configuration object used to generate the WriterFactory is instantiated as a singleton object. Consequently in order that the tool use a ConfigurationJml object instead of javadoc's ConfigurationImpl, the singleton is instantiated and initialized in Main, before other initialization code has a chance to create the ConfigurationImpl alternative.

Note that in this design, the standard javadoc doclet is still used.

Potential alternate design

This section describes an alternate, possibly future, design of jmldoc. This alternate design appears to be more aligned with the design of javadoc and its provision for doclet extensions, but also required more implementation and more duplication of javadoc code (meaning more maintenance as javadoc evolves).

The organization of javadoc's HTML output is controlled by an XML resource file (com/sun/tools/doclets/internal/toolkit/resources/doclet.xml). This file is parsed; for each XML element in the document a corresponding build method is called by reflection. For example, the doclet.xml file specifies that one part of the description of a ClassDoc is a ClassHeader. To generate the corresponding HTML, the buildClassHeader method of ClassBuilder is called by reflection.

So one means of adding additional information into the HTML is to provide a different (but largely duplicated) XML description file. In order to do that, one would create a new doclet that referenced that new XML file; the BuilderFactory and various builders (e.g. ClassBuilder) would need to be extended with methods that responded to XML document items calling for JML information to be generated. However, one still would need to extend (though somewhat differently) the various Writers that were extended in the previous design. Thus no work is saved by using the XML document and a new doclet; in fact, more classes need to be modified or extended.