JML

jml − Java Modeling Language (JML) specification checker

jml [option] ... file-or-directory-or-package [file-or-directory-or-package] ...
jml-gui [option] ... file-or-directory-or-package [file-or-directory-or-package] ...

The command jml and the graphical user interface version jml-gui both do type checking of Java Modeling Language (JML) specifications. JML is a behavioral interface specification language for Java(TM).

The jml script sets the CLASSPATH and then runs the Java class org.jmlspecs.checker.Main, which does both syntax and type checking of Java and JML files. That is it checks both Java source code and the JML annotations in source code and JML files.

The jml-gui script is similar, but just runs the Java class org.jmlspecs.checker.JmlGUI, which brings up a graphical user-interface to do the checking.

If the checker finds a error, the file name, line number, and column number where the error occurred are reported.

The jml script and the graphical user interface support the options described below. On the command line, one can give the options in the form described below; the graphical user interface has other ways to select files and set the options. Both options without arguments and options with arguments simply set the option as indicated by the description below. On the command line, multiple uses of the same option generally have no effect that is different than a single use of that option.

For the command line, each option has both a short form and two long forms. The long forms consists of one or two hyphens and a word. To avoid duplication, 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 separately. The short form consists of a hyphen and a single letter. 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 on the command line are case sensitive.

−−admissibility <String>

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.

−−Assignable, −A

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.

−−assignable, −a

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 "exceptional_behavior". A pure method is a method annotated with the JML modifier "pure". The default is to produce such caution messages.

−−classpath <directory-list>, −C <directory-list>

Use the given string as the CLASSPATH during checking. By default the value of the environment variable CLASSPATH is used instead.

−−debug, −c

Produces (copious) debugging information, intended for developers. The default is not to produce this information.

−−deprecation, −D

Test for deprecated members. The default is not to test for deprecated members.

−−excludefiles <pattern>

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.

−−filter <String>, −f <String>

Make the warning filter be the named class. The default is org.jmlspecs.checker.JMLDefaultWarningFilter.

−−generic, −G

Accept the Java 1.5 generic syntax. This feature is still experimental. The default is not to do this.

−−help, −h

Display the help information and exit. The default is not to do this.

−−keepGoing, −k

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.

−−multijava, −M

Accept MultiJava source code. The default is to not accept Multijava constructs.

−−nomultijava

Do not accept MultiJava source code. This turns off acceptance of Multijava constructs.

−−nonnull, −N

(Obsolete. To be removed soon.) Generate statistics with respect to the proportion of non-null declarations.

−−nonnulltypes, −j

Enable the use of the non-null type system which enables the static detection of potential null dereferences.

−−norecursive

Turn off −−recursive.

−−purity, −p

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.

−−Quiet, −Q

Shuts off all type checking informational messages. The default is produce these messages.

−−quiet, −q

Do not suppress information on compilation passes completed. This information is probably most useful to developers. The default is to suppress this information.

−−recursive, −R

Process all subdirectories of given directory and package arguments recursively. The default is not to process given subdirectories recursively.

−−relaxed, −r

Accept Relaxed MultiJava source code. The default is not to allow the special constructs in Relaxed MultiJava.

−−safemath, −s

Turns on safe math mode. This is an experimental feature, currently 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.

−−source <release-number>

Accept code containing source for the given Java version. When the release-number is "1.4", the compiler accepts code containing 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".

−−sourcepath <directory-list>, −S <directory-list>

Use the given path when searching for Java and annotation source files. A path is a list of directories separated by either colons (on Unix) or semicolons (on Windows). The default is to use the CLASSPATH.

−−universesx <String>, −E <String>

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 backslash).
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 program.

"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 standard 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.

−−universes, −e

Enable the default Universe type system features. This corresponds to the "−−universesx full" flag.
This option is disabled by default.

−−verbose, −v

Display verbose information during compilation. The default is not to display this information.

−−version, −V

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

−−warning=<int>, −w<int>

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.

−−Xnoversion

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.

−−xArrayNNTS, −J

Enable the experimental handling of array types in the non-null type system.

The CLASSPATH environment variable is used to find Java class and source files, as well as JML specification files.

The typical way to check files is as follows.

jml file1.java file2.java

The following checks all the Java and JML files in a directory, and only writes error messages and warnings, not status information.

jml -Q .

The following example is the same as the previous one, but recurses into all subdirectories of the directory .

jml --Quiet --recursive .

The jml script sets the CLASSPATH environment variable, but does not look at any -classpath option that might be used. If you use a -classpath 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.

If you are new to JML, you’ll want to look at some of the documents that ship with the system. You can access it from a web browser easily starting at the JML.html file in the top-level JML directory, $JMLDIR, i.e., from

$JMLDIR/JML.html

See also the the JML web page.

http://www.jmlspecs.org

java(1), javadoc(1), jmlc(1), jmldoc(1), jmlrac(1), jmlunit(1), jtest(1)

Copyright (c) 1999-2007 by Iowa State University

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 FITNESS 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.