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.
The jmldoc
tool is provided as a zip containing these
files:
openjml.jar
- a jar of the Java classes and
resources needed to run the tool
jmldoc
- a bash script that is a convenient driver
for the tool
README.html
- this file, containing a description
of the tool
OpenJDK-LICENSE-INFO
- the license under which the OpenJDK
is distributed and, by extension, applies to this jmldoc tool
java -classpath openjml.jar org.jmlspecs.openjml.jmldoc.Main options-and-files-and-package-names
-
character and may have an argument); the non-option
arguments are paths (absolute or relative to the current working directory)
of files or are names of packages that are rooted in one of the sourcepath
directories.
org.jmlspecs.openjml.jmldoc.Main.execute
javadoc
are valid for
jmldoc
. In addition,
jmldoc
recognizes these options (also reported by the
-help
option).
-specspath
: the argument to this option is the
path (in classpath form) in which to search for
specification files. The specification path is determined
by the first of these that is present:
-specspath
command-line option
-Dorg.jmlspecs.specspath=
option to the java execution
-sourcepath
command-line option
-classpath
command-line option
-Djava.class.path=
option to the java execution
CLASSPATH
environment variable at the time the java execution begins
-dir
: the argument to this option is a file-system path
to a directory; any java files found in this directory or its
subdirectories (recursively) are included as if they had been
listed individually on the command-line (the argument may also be
a file name, in which case it is included as is)
-dirs
: this option indicates that the following
command-line arguments are either file or directory names, up to
an argument that begins with a -
sign
-noInternalSpecs
: the jar file containing the
executable also contains a basic set of specifications of
core library classes (such as classes in
java.lang
). By default those specifications
are appended to the end of the specification path defined
above. If the -noInternalSpecs
option is
given, then these internal specs will not be added. The
user will then need to supply an alternate set of
specifications of basic library classes.
-noInternalRuntime
: The openjml tools require
some classes (e.g. those in the
org.jmlspecs.lang
package) to be available at
runtime. These are added by default to the end of the
classpath. If the -noInternalRuntime
option
is given, these classes are not added to the classpath;
the user will need to supply those manually.
-noCheckSpecsPath
: By default, a warning is
issued if a directory on the specification path does not
exist. If the -noCheckSpecsPath
option is
given, non-existent directories on the specs path are
silently ignored.
jmldoc
output.
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????
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.
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.