JMLC

jmlc − compile JML annotated Java files with runtime assertion checks

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

The command jmlc and the graphical user interface jmlc-gui compile Java(TM) files (and JML specification files) with their JML annotations turned into runtime checks. It thus acts as a Java compiler, but with the additional effect of enabling automatic checks of assertions when the code is executed. The output is a .class file, which can be treated in much the same way as the output of any java compiler.

Note, however, that the .class files produced by jmlc depend on classes in the org.jmlspecs.jmlrac.runtime package (and also in the org.jmlspecs.models package if those classes are used in assertions), which therefore also need to be loaded. These can be obtained from the file JML/bin/jmlruntime.jar in the JML release. The jml release provides the script jmlrac which adds this jar file to the CLASSPATH and then runs java, to facilitate this loading process.

The class files produced by jmlc can be mixed with those generated by other Java compilers, but for maximal checking, one should compile all classes together using a form such as jmlc.

jmlc also processes JML specification files (e.g. .spec files). In this case it generates a wrapper class that includes all of the runtime assertion checks, but delegates the actual operation of a method to an instance of the original class. This mechanism is useful for testing classes for which the user only has .class files and .spec files that purport to specify the behavior of the .class files. In this case, the −packageName option will usually be needed, in order to place the generated, runtime-assertion-checking .class file in a different package than the

The jmlc script sets the CLASSPATH and then runs the Java class org.jmlspecs.jmlrac.Main, which does both syntax and type checking of Java and JML files, and then generates the runtime assertion enabled JVM bytecode in class files for each of the Java files (i.e., for each .java file).

The jmlc-gui script is similar, but just runs the Java class org.jmlspecs.jmlrac.RacGUI, which brings up a graphical user-interface to do the compilation.

If the compiler finds an error, the file name, line number, and column number where the error occurred are reported. In such cases, by default, processing stops and no output will be produced for the files.

Note that the compiler recognizes Java source files generated by itself (using the −−print, −P option, see below) and does not compile them even if they are explicitly listed as command-line arguments or found in a directory (or subdirectory) whose name is given as a command-line argument. Similarly, it does not try to compile Java source files generated by jmlunit. That is, it does not compile files whose names end with the suffix ‘_JML_Test.java’ or ‘_JML_TestData.java’. (These files should be compiled with a normal java compiler, such as javac or mjc.)

For a tutorial introduction on the basics of using jmlc, see the EXAMPLES section below.

The jmlc 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. 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. See [1] for details. 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 compilation. By default the value of the environment variable CLASSPATH is used instead.

−−debug, −c

Produces (copious) debugging information. The default is not to produce this information.

−−defaultNonNull, −n

Make reference paramenters, fields and method return types non_null by default. (Enabled by default)

−−deprecation, −D

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

−−destination <directory>, −d <directory>

Writes files (such as bytecode class files) in a subdirectory corresponding to the file’s package name, relative to the named destination directory. The default is to write such files in the directory in which the source files reside (which may not be the current directory).

−−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.jmlrac.JMLRacWarningFilter. If you do not want to see warnings about certain features not being executable, then you should use 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.

−−mustBeExecutable, −V

By default, non-executable Boolean expressions contained in assertions are assumed to be true. Use this option to interpret such assertions as false (which can help pin-point such expressions, especially since the executability of some expressions is only determined at runtime). This option is only meaningful when "−−oldSemantics" is not used.

−−oldSemantics, −O

By default, an assertion is taken as valid if it is "strongly validity", i.e. it is both defined and true [2,3]. Use this option to revert to the former semantics [4].

−−neutralContext, −o

Interpret expressions within conditional and logical or expressions using a neutral context, so that expressions like

   x.length > 0 || true

will be false when x is null. The default is to use the contextual interpretation, which, for example, makes the above expression be true, as dictated by the normal rules of logic.

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

−−noredundancy, −Y

Do not compile redundant specifications into runtime checks. Examples of redundant specifications are requires_redundantly, ensures_redundantly, signals_redundantly, invariant_redundantly, constraint_redundantly, assume_redundantly, and assert_redundantly. The default is to compile all redundant specifications into runtime checks.

−−noreflection, −F

Do not use Java’s reflection facility to inherit specifications from superclass and superinterfaces. The default is to use Java reflection for such inheritance. When reflection is used, calls made using Java’s reflection API are made to superclass’s and superinterfaces’s assertion check methods such as pre- or postcondition check methods. However, when this option is used, it suppresses this behavior, and instead code is generated that makes direct calls. Thus calls are generated at compile time directly to the superclass’s and superinterfaces’s assertion check methods. The benefit of not using reflection for specification inheritance is that the generated code is a lot faster; however, you have to make sure that the superclass and superinterfaces are either listed in the command-line as input files, or that they have already been compiled with jmlc and that the corresponding .class files are available via the CLASSPATH.

−−nowrite, −W

Only check the given files, do not compile to bytecode and do not write output files. The default is to compile to bytecode and write to the output files.

−−packageName, −N

The name of the package for the generated classes. The default is the same package as the source files. An empty string argument produces generated classes in the unnamed package. If the argument ends in a ’+’, then the argument is prefixed (with a separating ’.’ character replacing the ’+’) to the package name of the source file.

−−print, −P

Prints Java source code (with runtime annotation code included) instead of compiling to bytecode. The file name used for the output is formed from the Java source code file name with the additional suffix ‘.gen’. For example, ‘Foo.java’ is printed into a file ‘Foo.java.gen.’. The default is instead to compile to bytecode.

−−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. The default is to suppress this information.

−−recursive, −R

Process all subdirectories of given directory and package arguments recursively.

−−relaxed, −r

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

−−recursiveType, −t

Force typechecking of recursively referenced types. There are some occasions when it is necessary to typecheck recursively referenced types, e.g., to determine an applicable represents clause for a model field. The default is to not typecheck recursively referenced types.

−−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 typical way to compile file for runtime-assertion checking is as follows.

jmlc *.java

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

jmlc -Q .

The following example is the same as the previous one, but recurses into all subdirectories of the directory ’.’. Note that the resulting .class files will be found in the same directories as the corresponding .java files.

jmlc --Quiet --recursive .

The following example shows the use of the -d option. Suppose that the current directory contains the Java source files for the package org.jmlspecs.samples.stacks (i.e., all the Java source files in the current directory name that as their package). Then the following compilation will write the class file BoundedStack.class into the directory temp/org/jmlspecs/samples/stacks.

jmlc -dtemp BoundedStack.java

To run programs compiled with jmlc you need to have various runtime classes in your CLASSPATH. The jmlrac(1) script provides a way to do this automatically. See its manual page for more details.

If you are using jmlc with the jmlunit(1) tool, see the jmlunit manual page for more examples and explanations.

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

The jmlc 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.

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

[1] P. Mueller, A. Poetzsch-Heffter and G. Leavens, "Modular Invariants for Layered Object Structures", 2004.
[2] P. Chalin, "A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler". Proceedings of the International Conference on Software Engineering (ICSE), Minneapolis, MN, USA, 2007. [3] F. Rioux and P. Chalin, "Effective and Efficient Runtime Assertion Checking for JML Through Strong Validity". Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (FTfJP’07), Berlin, Germany, 2007. [4] G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok, "How the design of JML accommodates both runtime assertion checking and formal verification", Science of Computer Programming, 55(1-3):185-208, 2005.

Copyright (c) 2001-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.