|PREV PACKAGE NEXT PACKAGE||FRAMES NO FRAMES|
|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|
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 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.
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.utiland its subpackages - the multijava compiler
tools.jar. If the command
javap com.sun.tools.doclets.standard.Standardsuccessfully lists the API for the
Standardclass, then your
CLASSPATHcontains the appropriate reference.
CLASSPATH appropriately set
(it must include the paths to packages you wish to document), execute
java org.jmlspecs.jmldoc.Main options files packages
Alternatively, one can be specific about classpaths and write
java -classpath cp1 org.jmlspecs.jmldoc.Main -classpath cp2 -sourcepath cp3 ...
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.
-author: causes information in
@authortags to be put into the html pages; the default is to omit the information
-bootclasspathclasspath : specifies the set of directories and jar files in which the Java system classes are found; the default is system specific.
-bottomstring : 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.
-charsetstring : specifies the HTML character set for the document as given in the usual META tag; the default is to omit the META html tag.
-classpathpathlist : 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
-ddirectorypath : 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
-docencodingname : 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
-docletclass : uses the given (fully-qualified) class as the doclet class to use instead of the
MjdocStandardclass. See the doclet API for more information about writing new doclets.
-docletpathclasspathlist : specifies a path to or jar file containing the doclet specified in the
-docletoption. The default is the value of
-classpath(NOT IMPLEMENTED - add the doclet location to the classpath instead).
-doctitlestring : uses the given string as the displayed title in the generated overview html page; the default is no title.
-encodingname : specifies the encoding name of the source files, otherwise uses a platform-specific default
-excludepkglist : specifies a list of packages to exclude from being documented
-excludedocfilessubdirname1:name2:... : exclude any listed doc-files subdirectories
-extdirsdirectorylist : specifies the directories where extension classes are found (NOT IMPLEMENTED - use bootclasspath instead)
-footerstring : 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
-groupgroupheading 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.
-headerstring : 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
-helpfilefilepath : 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
-linkurl : specifies a url (either
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
-linkoptions. It is required that there be a file named
package-listat the specified url; this file contains the list of packages that are documented at that location.
-linkofflineurl url-or-directory : as for the
-linkoption, 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-listfile 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
-localelocale-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: prevents the generation of the
deprecated-list.htmlfile, 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
-noqualifiername1:name2:... : exclude the list of qualifiers from the output
-nosince: prevents the listing of any information from
-notree: omits the class/interface tree from the generated documentation
-overviewpath/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
-sourcepathrefers 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 (
-private: These control which classes and class members are documented on the html pages, according to their declared access level. The default is
-quiet: Turns off any informational messages from the javadoc doclet api (Now equivalent to
-serialwarn: causes warnings to be generated for missing
@serialtags (NOT IMPLEMENTED)
-sourcerelease : provide source compatibility with specified release
-sourcepathpathlist : the set of root locations to search for the packages specified on the command-line. The default is the value of
-splitindex: if an index is generated, generates it as a number of smaller files instead of one large file
-subpackagessubpkglist : specifies subpackages to recursively load
-stylesheetfilefilepath : 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.
-tagname:location:header : specifies a single argument custom tag
-tagletname : specifies a fully-qualified name of a taglet class
-tagletpathpathlist : 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
@versiontags to be put into the html pages
-windowtitlestring : 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.
-Q: shuts off any jmldoc informational messages, including the effect of
--quiet; this is now equivalent to
-Cclasspath : specifies the root directories where referenced classes and packages are found; equivalent to
--deprecation: not applicable to jmldoc (in mjc it prevents deprecated methods from being called); use
-nodeprecatedabove to avoid listing deprecated classes and methods in the generated documentation
-ddirectory : equivalent to the
-djavadoc option; it causes all output files to be created relative to the given directory; the default is the current directory.
--docpathdirectorylist : pathlist in which to find javadoc files (provides functionality similar to
-link, but all in one pathlist in one option)
-h: simply prints out usage information and terminates, without processing any files (equivalent to
--norecursive: disables the
-recursiveoption (the default is non-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
-subpackageoption in javadoc 1.4 for a slightly different but similar functionality.
-U: show both implicit and explicit promotions (widening coercions) in rendered annotations; if false (the default), neither are shown.
-Sdirectorylist : equivalent to
-V: displays the version number of the jmldoc program and terminates
-wint : controls the pickiness of the warnings produced by jmldoc, in an undocumented way
--fcnsarg : 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. [
-allis experimental and incomplete ]
-M: enables multijava extensions (default is enabled)
--nomultijava: disables multijava extensions
-c: enables the production of copious debugging information
-fqualifiedName : names a filter to filter error and warning messages
-k: instructs jmldoc to continue on after reporting errors, even at the risk of runtime exceptions
-q: enables the printing of timing information about each compilation phase
-v: enables the printing of tracing information about each compilation phase
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
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.
--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.
@throwstags 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.
-overviewoption 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.
-docletpathoption is not implemented.
-extdirsoption is not implemented.
-localeoption is not implemented.
-subpackagesoption is not implemented.
-excludeoption is not implemented.
-excludedocfilessubdiroptions are not implemented.
|PREV PACKAGE NEXT PACKAGE||FRAMES NO FRAMES|