JMLDOC(l)							    JMLDOC(l)



1mNAME0m
       jmldoc - generate HTML pages from JML and Java files

1mSYNOPSIS0m
       1mjmldoc	22m[option]  ... file-or-package-or-directory [file-or-package-or-
       directory] ...
       1mjmldoc-gui 22m[option] ... file-or-package-or-directory  [file-or-package-
       or-directory] ...

1mDESCRIPTION0m
       The  command 1mjmldoc 22mand the graphical user interface version 1mjmldoc-gui0m
       generate HTML (web) pages from JML annotated Java(TM)  and  JML	files.
       This  is similar to Javadoc, but 1mjmldoc 22munderstands JML specifications,
       and includes this information in the generated HTML pages.  The program
       also  type  checks  the	JML specifications to some extent and combines
       annotations across refinement files.  The output is a set of HTML files
       that can be browsed using a web browser.

       The  1mjmldoc  22mscript	sets  the  CLASSPATH  and then runs the Java class
       org.jmlspecs.jmldoc.Main, which does both syntax and type  checking  of
       Java and JML files, and then generates the HTML pages.

       The 1mjmldoc-gui 22mscript is similar, but just runs the Java class org.jml-
       specs.jmldoc.JmldocGUI, which brings up a graphical  user-interface  to
       do the HTML generation.

       This  version  of jmldoc is compatible with Java 1.4.1 and not with any
       earlier versions of the Java developement kit.

       The non-option arguments may be	either	a  filename,  a	dot-separated
       package	name,  or a directory name.  A simple name is interpreted as a
       package name.  When packages or directories are given, jmldoc processes
       all  files in the named directory with either a .java suffix or a legal
       refinement suffix (e.g. .refines-java).

1mOPTIONS0m
       This program supports the options described below.  There are two kinds
       of options, some contributed by javadoc and some contributed by the mjc
       parser that is used by jmldoc.

       Options from javadoc consist of a single hyphen and  the	name  of  the
       option;	if there is an argument to the option it is separated from the
       name of the option by whitespace.

       Options contributed by the mjc parser have both a long and short	form.
       The  short  forms  consist  of a single hypen and a single letter.  The
       long forms consist of one or two hyphens and a word.  To avoid duplica-
       tion,  we  only	show  the long forms with two hyphens, since these are
       unambiguous; however one can use the forms  with	a  single  hyphen  if
       desired.	To  avoid  ambiguity between multiple short form options and
       the long form with a single hyphen, one should give each	option	sepa-
       rately.	In  the  synopsis  below, the long form is separated from the
       short form by a comma (,), but in actual usage, you would pick  one  of
       these forms and not use the comma.

       Note that options given on the command line are case sensitive.

       1m--ImplicitPromotion, -i0m
	      This  disables  implicit promotion (to \bigint).	This promotion
	      only occurs within specifications and in	specification  expres-
	      sions,  and  does	not affect Java code.	The default is to have
	      such implicit promotions to \bigint.

       1m--Quiet, -Q, -quiet0m
	      Shuts off all type checking informational messages.  The default
	      is to produce these messages.  (The jmldoc --Quiet is now equiv-
	      alent to the javadoc  -quiet,  but  not  to  the	jmldoc	option
	      --quiet).

       1m--admissibility <String>0m
	      Checks the admissibility of invariants and represents clauses in
	      accordance with a certain	proof	technique.  For	more  details
	      about  admissibility  see "Modular Invariants for Layered Object
	      Structures" by P. Mueller, A. Poetzsch-Heffter and  G.  Leavens,
	      2004.
	      Statics (static invariants, static represents clauses and static
	      fields appearing in one of the former) and method calls  (in  an
	      invariant or a represents clause) are not yet supported.

	      Available option strings:

		     "none"
			     No admissibility checks are performed.
			     This is the default.

		     "classical"
			     Admissibility checks of invariants and represents
			     clauses are done in accordance with the classical
			     modular proof technique.
			     See the above mentioned paper for details.

		     "ownership"
			     Admissibility checks of invariants and represents
			     clauses are done in accordance with the ownership
			     proof   technique,	using	the  UTS  information.
			     Therefore this option only makes sense if the UTS
			     is enabled at least for parsing and typechecking.
			     Additionally fields and methods  are  checked  to
			     ensure subclass separation.
			     For  further  details  see	the  above  mentioned
			     paper.

       1m--Assignable, -A0m
	      Turn off errors that are otherwise given when a method  with  an
	      "assignable"  clause calls methods that do not have "assignable"
	      clauses.	The default is to produce such messages.

       1m--assignable, -a0m
	      Turn off caution messages for heavyweight specification cases of
	      non-pure methods that have no "assignable" clause. A heavyweight
	      specification case is a specification case that starts with  one
	      of   the	keywords  "behavior",  "normal_behavior",  or  "excep-
	      tional_behavior".	A pure method is a method annotated with  the
	      JML  modifier  "pure".   The  default is to produce such caution
	      messages.

       1m--classpath <directory-list>, -C <directory-list>0m
	      Use the given string as the CLASSPATH.  By default the value  of
	      the environment variable CLASSPATH is used instead.

       1m--debug, -c0m
	      Produces (copious) debugging information.	The default is not to
	      produce this information.

       1m--deprecation0m
	      Test for deprecated members.  The default is  not	to  test  for
	      deprecated members.  (Not applicable to jmldoc)

       1m--destination <directory>, -d <directory>0m
	      Writes  HTML files in a subdirectory corresponding to the file's
	      package name, relative to the named destination directory.   The
	      default is the current working directory.

       1m--docpath <directory-list>0m
	      A	path  (directory list separated by the path separator charac-
	      ter) that tells where to find javadoc files.  Using this	option
	      is  equivalent  to a series of -link options each specifying one
	      directory from the directory list.

       1m--excludefiles <pattern>0m
	      A pattern (regular expression) for file names  to	exclude  from
	      processing.  By default this is the pattern
		 _JML_Test[\044.]
	      which  means that file names that contain the strings _JML_Test.
	      or _JML_Test$ are not processed (044 is the  octal  code	for  a
	      dollar  sign),  unless  they are referred to by other files that
	      are processed.  The regular expressions that  can	be  used  are
	      described in the javadocs for the type java.util.regexp.Pattern.
	      For example, when building the JML  documentation,  we  use  the
	      pattern
		 _JML_Test[\044.]|TestSuite\.[^.]+
	      which  excludes files with names like TestSuite.java, as well as
	      the _JML_Test files.  This was necessary	for  us,  becuase  the
	      TestSuite.java files reference the types named _JML_Test.

       1m--fcns <option>0m
	      Used to specify the treatment of external functions in MultiJava

       1m--filter <String>, -f <String>0m
	      Make the warning filter be the  named  class.   The  default  is
	      org.jmlspecs.checker.JMLDefaultWarningFilter.

       1m--generic, -G0m
	      Accept  the  Java	1.5  generic  syntax.	This feature is still
	      experimental.  The default is not to do this.

       1m--help, -h0m
	      Display the help information and exit.  The default is not to do
	      this.

       1m--keepGoing, -k0m
	      Keep going when errors are encountered.  Be warned that this may
	      cause the tool to die with an exception.	The default is to  not
	      keep going.

       1m--multijava, -M0m
	      Accept MultiJava source code.  The default is to not accept Mul-
	      tijava constructs.

       1m--nomultijava0m
	      Do not accept MultiJava source code.  This turns off  acceptance
	      of Multijava constructs.

       1m--norecursive0m
	      Do not recurse into subdirectories of command-line arguments

       1m--purity, -p0m
	      Do  not check for pure-ness of methods referenced in assertions.
	      A method is considered to be pure if it is  annotated  with  the
	      JML modifier "pure".  The default is to check for purity.

       1m--quiet, -q0m
	      Do  not  suppress	information  on compilation passes completed.
	      The default is to suppress this information.

       1m--recursive, -R0m
	      Process all subdirectories of given directory or	package	argu-
	      ments  recursively.   The	default is not to process subdirecto-
	      ries.

       1m--relaxed, -r0m
	      Accept Relaxed MultiJava source code.  The  default  is  not  to
	      allow the special constructs in Relaxed MultiJava.

       1m--safemath, -s0m
	      Turns  on	safe math mode. This is an experimental feature, cur-
	      rently under development, in which the  checker  will  report  a
	      compile-time  error  if  the  evaluation	of a constant integral
	      expression causes an overflow.  The default  is  not  to	report
	      such errors.

       1m--showPromotion, -U0m
	      Shows  implicit  and  explicit  coercions	in  annotations.  The
	      default is not to show such promotions.

       1m--source <release-number>0m
	      Accept code containing source for the given Java version.	When
	      the  release-number is "1.4", the compiler accepts code contain-
	      ing Java	1.4  assert  statements,  and  treats  `assert'	as  a
	      reserved	word in Java code.  The default is "1.3", meaning that
	      `assert' is not a reserved word in Java code (although it is  in
	      annotations).   In  some future release of JML, the default will
	      change to "1.4".

       1m--sourcepath <directory-list>, -S <directory-list>0m
	      Use the given path when searching for packages specified on  the
	      command  line.   A  path	is  a list of directories separated by
	      either colons (on Unix) or semicolons (on Windows).  The default
	      is to use the CLASSPATH. (Equivalent to -sourcepath)


       1m--universesx <String>, -E <String>0m
	      Specify  the  degree  of	support	for  the Universe type system
	      (UTS).

	      Available option strings:

		     "no"
			     UTS features are disabled	and  no	keywords  are
			     reserved.
			     Only the \xxx version of the keywords are allowed
			     (all UTS keywords have to be prefixed by a	back-
			     slash).
			     This is the default.

		     "parse"
			     the UTS keywords are reserved and parsed.

		     "check"
			     UTS typechecking is performed.

		     "dynchecks"
			     code  for	UTS  runtime checks (for downcasts and
			     array updates) is generated.
			     This also turns on the  "check"  option,  because
			     the  runtime  checks  rely on a type-checked pro-
			     gram.

		     "purity"
			     purity of methods is checked with a  conservative
			     method,  which  might forbid some methods that do
			     not modify existing objects.

		     "xbytecode"
			     Universe type information is  stored  in  special
			     bytecode attributes.
			     This also turns on the "check" option, because it
			     is important that the stored information is type-
			     checked.
			     The resulting class-file is compatible with stan-
			     dard Java VMs.

		     "annotations"
			     Universe type information is  stored  in  Java  5
			     annotations.
			     This also turns on the "check" option, because it
			     is important that the stored information is type-
			     checked.
			     The  resulting class-file is compatible with Java
			     5 VMs.

		     "full"
			     all  UTS  features	except   "annotations"   are
			     enabled; this corresponds to the --universes flag
			     below.

	      The options "no" and "full"  must	be  used  alone.   All	other
	      options  can  be combined by separating them with commas.	First
	      all options are turned off and then the given options  (and  the
	      options  implicitly  turned  on by the given options) are turned
	      on.

       1m--universes, -e0m
	      Enable the default Universe type system features.	This	corre-
	      sponds to the "--universesx full" flag.
	      This option is disabled by default.


       1m--verbose, -v0m
	      Display  verbose information during compilation.	The default is
	      not to display this information.

       1m--version, -V0m
	      Instead of doing anything	else,	print  the  checker's  version
	      information  on standard output and exit.	The default is not to
	      do this.

       1m--warning=<int>, -w <int>0m
	      Set the `pickiness' of warnings displayed to the given  integer.
	      The  default is 1.  Using 2 generates more picky warnings, and 3
	      more picky still.

       1m--Xnoversion0m
	      Omits printing the version in help messages, which is useful for
	      regression  testing (but not normally by users).	The default is
	      to print the version in help messages.

       The following options are inherited from javadoc (see the javadoc docu-
       mentation  for  more detail).  The option names (but not the arguments,
       nor the options listed above) are case-insensitive.

       1m-author0m
	      Causes information in @author tags to be put  into  html	pages;
	      the default is to omit them

       1m-bootclasspath <path>0m
	      Specifies the sequence of directories and jar files in which the
	      Java system classes are found; the default is system specific

       1m-bottom <String>0m
	      A string of HTML content to be placed below the lower navigation
	      bar

       1m-breakiterator0m
	      In  javadoc specifies how to determine the summary sentence of a
	      comment.	The option in ignored in jmldoc	since	jmldoc	always
	      behaves like javadoc with -breakiterator enabled.

       1m-charset <String>0m
	      Specifies	the  HTML  character set for the document as given in
	      the META tag; the default is to omit the META tag

       1m-classpath <path>0m
	      The sequence of root lcoations (directories and jar files)  that
	      are  searched  for  classes  referenced  in classes and packages
	      listed on the command line; the default  is  the	value  of  the
	      CLASSPATH environment variable

       1m-d <directory>0m
	      The  location  in	which output files are written (equivalent to
	      --destination); the default is the current directory.

       1m-docfilessubdirs0m
	      Recursively copy doc-file subdirectories

       1m-docencoding <name>0m
	      Specifies the html encoding for generated files; the default  is
	      the default encoding of the local java virtual machine.

       1m-doclet <classname>0m
	      Specifies a fully-qualified class name that is to be used as the
	      doclet instead of jmldoc

       1m-docletpath <path>0m
	      Specifies a path in which to find	the  doclet  in  the  -doclet
	      option;  the  default is the value of -classpath; (option is NOT
	      IMPLEMENTED)

       1m-doctitle <String>0m
	      Specifies the title to display in the  generated	overview  html
	      page; the default is no title

       1m-encoding <name>0m
	      Specifies	the encoding name of the source files; otherwise uses
	      a platform-specific default

       1m-exclude <pkglist>0m
	      Specify a list of packages to exclude

       1m-excludedocfilessubdir <name1>:...0m
	      Exclude an doc-files subdirectories with the given names

       1m-extdirs <path>0m
	      Specifies the path to search for extension classes; the  default
	      is to use the bootclasspath; NOT IMPLEMENTED

       1m-footer <String>0m
	      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

       1m-group <groupheading> <packagepatternlist>0m
	      Allows the organization of the packages listed on	the  overview
	      page  to	be  grouped in specified sections, as described in the
	      javadoc documentation; by default all packages are in one group

       1m-header <String>0m
	      A string of HTML content to be placed to the right of the	upper
	      navigation bar

       1m-help	22mPrints  out	the options and usage and terminates (equivalent to
	      --help)

       1m-helpfile <file>0m
	      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  generates
	      its own file at a hard-coded filesname.  The given file is found
	      relative to the current directory.

       1m-J<flag>0m
	      Specifies runtime system options (note no white space after  the
	      J)

       1m-link <url>0m
	      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 'pack-
	      age-list' at the specified url; this file contains the  list  of
	      packages whose documentation is at that location.

       1m-linkoffline <url> <url-or-directory>0m
	      Specifies the location (as does the -link option) of class docu-
	      mentation for classes not being documented in the current execu-
	      tion  of	jmldoc.	In this case, the url-or-directory gives the
	      location of the package-list file	that  contains	the  list  of
	      packages	that are documented at the location url.  The url need
	      not be available at the time the documentation is generated.

       1m-linksource0m
	      Generate links to the source files, rewritten in HTML.

       1m-locale <locale-name>0m
	      Specifies the locale to be used for rendering text  (place  this
	      option first) [NOT IMPLEMENTED in jmldoc]

       1m-nocomment0m
	      Suppress description and tags, generating only declarations

       1m-nodeprecated0m
	      Prevents	the generation of any documentation of deprecated ele-
	      ments (as well as doing what -nodeprecatedlist does)

       1m-nodeprecatedlist0m
	      Prevents the generation of the deprecated-list.html file,	which
	      contains a list of deprecated elements

       1m-nohelp0m
	      Prevents the generation of a help file

       1m-noindex0m
	      Prevents the generation of an index

       1m-nonavbar0m
	      Causes  the documentation to omit the header, footer and naviga-
	      tion bars

       1m-nooverview0m
	      Prevents an overview file from being generated  when  more  than
	      one package is being documented

       1m-noqualifier <name1>:<name2>:...0m
	      Exclude the listed qualifiers from the output

       1m-nosince0m
	      Prevents the listing of any information from @since tags

       1m-notree0m
	      Omits the class/interface tree from the generated documentation

       1m-overview <file>0m
	      Causes  jmldoc  to create an overview page using the information
	      in the given file, which is found relative to  the  -sourcepath.
	      In  jmldoc,  an overview file is created by default if more than
	      one package is being documented.	(Despite the javadoc  documen-
	      tation,  javadoc 1.3 looks for the overview file relative to the
	      current directory).

       1m-public, -protected, -package, -private0m
	      These options control which classes and class members are	docu-
	      mented, according to their declared access level

       1m-quiet 22mSuppress doclet-produced informational messages.  This option is
	      now equivalent to --Quiet.

       1m-serialwarn0m
	      Causes warnings to be generated for missing  @serial  tags  (NOT
	      IMPLEMENTED)

       1m-sourcepath <path>0m
	      The sequence of directories and jar files to be searched for the
	      packages that are specified on the  command  line;  the  default
	      value is the value of -classpath

       1m-splitindex0m
	      Causes  the index, if it is generated, to consist of a number of
	      files instead of one long file

       1m-stylesheetfile <file>0m
	      The file to use instead of the default stylesheet file.  It will
	      be  copied  to  the root of the documentation set (retaining the
	      same filename).  The file	is  found  relative  to  the  current
	      directory.

       1m-subpackages <subpkglist>0m
	      Specify subpackages to recursively load

       1m-tag <name>:<locations>:<header>0m
	      Specify single-argument custom tags

       1m-taglet0m
	      The fully qualified name of a custom taglet

       1m-tagletpath0m
	      The search path for taglet .class files

       1m-use	22mCauses  the	use  information  pages	(one per class and one per
	      package) to be generated

       1m-verbose0m
	      A javadoc option that has no effect in jmldoc

       1m-version0m
	      Causes information in @version tags to be put in	the  generated
	      pages

       1m-windowtitle <string>0m
	      Uses  the	given	string	in the TITLE tag of the generated html
	      pages (so that it appears in the	title  bar  and	bookmarks  or
	      favorite	lists of the html browser).  The javadoc documentation
	      says that the default is the value of -doctitle, but javadoc 1.3
	      (and  jmldoc) actually produces by default a title of "Generated
	      Documentation (Untitled)" on the frame-style overview  page  and
	      an empty title on other pages.

       1m-x	22mPrints out a list of special (javadoc) options

       1m-xnodate0m
	      A	special  option  tha  causes  html  pages  to have the string
	      'TODAY' instead of a current date and time


1mEXAMPLES0m
       Here is an example of running jmldoc on the packages that make  up  the
       MJ  compiler.   (Here  $HOME is the root of the MJ directory containing
       the MJC source code).
	      rm -fr $HOME/MJ/javadocs
	      jmldoc -Q -private -d $HOME/MJ/javadocs \
		-link file:/cygwin/usr/local/jdk1.4/docs/api \
		-link file:/cygwin/usr/local/antlr/javadocs \
		--sourcepath $HOME/MJ  \
		org.multijava.dis org.multijava.javadoc org.multijava.mjc \
		org.multijava.mjdoc org.multijava.util org.multijava.util.backend \
		org.multijava.util.classfile org.multijava.util.compiler \
		org.multijava.util.jperf org.multijava.util.lexgen \
		org.multijava.util.msggen org.multijava.util.optgen \
		org.multijava.util.optimize org.multijava.util.testing

       The options used in the above  invocation  of  jmldoc  make  jmldoc  be
       quiet,  document	all  members  (including private ones) of classes and
       interfaces, write the HTML files relative to $HOME/MJ/javadocs, link to
       existing	HTML  files  for  the JDK and ANTLR, and find listed packages
       relative to $HOME/MJ.

1mENVIRONMENT0m
       The 1mCLASSPATH 22menvironment variable is  used	to  find  Java	class	and
       source files, as well as JML specification files.

1mBUGS0m
       The 1mjmldoc 22mscript sets the CLASSPATH environment variable, but does not
       look at any -classpath option that might be used.  If you use a -class-
       path  option,  then  you must explicitly include paths to the jar files
       and directories that this script would have otherwise included.	On the
       other  hand, this allows you to override the default orderings for such
       jar files and directories.

1mSEE ALSO0m
       java(1), javadoc(1), jml(1), jmlc(1), jmlrac(1), jmlunit(1),  jtest(1),
       the  html  documentation	at  org/jmlspecs/jmldoc/package.html  or  the
       overview javadoc documentation for the jmldoc package

1mAUTHOR0m
       The current version of jmldoc was written by David Cok, building on the
       source  files  of Sun MicroSystems' doclet API and on the parsing capa-
       bilities of the MultiJava compiler and the JML checker.	The  original
       concept was implemented in the first version by Arun Raghavan.

1mCOPYRIGHT0m
       Copyright (c) 2002 by Iowa State University and David Cok

       JML  is	free  software; you can redistribute it and/or modify it under
       the terms of the GNU General Public License as published	by  the  Free
       Software	Foundation;  either  version 2, or (at your option) any later
       version.

       JML is distributed in the hope that it will be useful, but WITHOUT  ANY
       WARRANTY;  without even the implied warranty of MERCHANTABILITY or FIT-
       NESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License  for
       more details.

       You should have received a copy of the GNU General Public License along
       with JML; see the file COPYING.	If not, write  to  the	Free  Software
       Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.



4th Berkeley Distribution$Date: 2005/12/22 20:57:45 $		JMLDOC(l)