Using the command-line tool

Basic example

OpenJML can be invoked as a command in a command-shell environment. It requires that Java 1.7 and the java command are available. THe current release of OpenJML cannot be run with Java 8 or 9. The basic form is standard:

java -jar openjml.jar options files

The options and files may be intermingled. The files are listed just as they would be in a java compilation command; they may include .java and .jml files. files may include folders; listing a folder is equivalent to listing all .java and .jml files within the folder and its subfolders. Files and folders are written as absolute paths or as paths relative to the current working directory. [TBD - is the -dir option necessary?] The openjml.jar library need not be in the current working directory (as in the example above). You may give a relative or absolute path to the library instead.

Using directory paths

The discussion here describes how OpenJML uses the classpath, sourcepath, and specifications path to find class, source and specifications files.

Exit codes

The exit codes from the command-line version of OpenJML have these meanings:

Command-line options

The commandline options follow the style of the OpenJDK compiler -- they begin with a single hyphen.

OpenJML (but not OpenJDK) options that require a parameter may either use an = followed directly by the argument or may provide the argument as the subsequent entry of the argument list. For example, either --racbin=output or --racbin output is permitted. If the argument is optional but present, the = form must be used.

Options that are boolean in nature can be enabled and disabled by either
1) adding a prefix -no, as in -showRacSource and -no-showRacSource
2) using the = form, as in -showRacSource=true and -showRacSource=false

Informational options

Relevant Java compiler options

All the OpenJDK compiler options apply to OpenJML as well. The most commonly used or important OpenJDK options are listed here.

OpenJML operational modes (mutually exclusive)

JML operational modes (mutually exclusive)

Options applicable to all JML tasks

Options related to parsing and type-checking

Options specific to static checking

Options specific to runtime checking

Options that control output