Using OpenJML class, source, and specifications paths

Finding source, class and specification files

When a Java compiler compiles source files, it considers three types of files:
  • Source files listed on the command-line
  • Other source files referenced by those listed on the command-line, but not on the command-line themselves
  • Already-compiled class files
The OpenJML tool considers the same files, but also needs
  • Specification files associated with classes in the program

The OpenJML tool behaves in a way similar to a typical Java compiler, making use of three directory paths - the classpath, the sourcepath, and the specspath. These paths are standard lists of directories or jar files, separated either by colons (Unix) or semicolons (Windows). Java packages are subdirectories of these directories.

  • classpath: The OpenJML classpath is set using one of these alternatives, in priority order:
    • As the argument to the OpenJML command-line option -classpath
    • As the value of the Java property org.jmlspecs.openjml.classpath
    • As the value of the system environment variable CLASSPATH
  • sourcepath: The OpenJML sourcepath is set using one of these alternatives, in priority order:
    • As the argument of the OpenJML command-line option -sourcepath
    • As the value of the Java property org.jmlspecs.openjml.sourcepath
    • As the value of the OpenJML classpath (as determined above)
  • specspath: The OpenJML specifications path is set using one of these alternatives, in priority order:
    • As the argument of the OpenJML command-line option -specspath
    • As the value of the Java property org.jmlspecs.openjml.specspath
    • As the value of the OpenJML sourcepath (as determined above)

Note that with no command-line options or Java properties set, the result is simply that the system CLASSPATH is used for all of these paths. A common practice is to simply use a single directory path, specified on the command-line using -classpath, for all three paths. The paths are used as follows to find relevant files:

  • Source files listed on the command-line are found directly in the file system. If the command-line element is an absolute path to a .java file, it is looked up in the file system as an absolute path; if the command-line element is a relative path, the file is found relative to the current working directory.
  • Classes that are referenced by files on the command-line or transitively by other classes in the program, can be found in one of two ways:
    • The source file for the class is sought as a sub-file of an element of the sourcepath.
    • The class file for the class is sought as a sub-file of an element of the classpath.
    If there is both a sourcefile and a classfile present, then TBD.
  • The OpenJML tool also looks for a specification file for each source or class file used in the program. The specification file is a Java-like file that has a .jml suffix, but otherwise has the same name and Java package as the class that it specifies. The specification file used is the first .jml file with the correct name and package found in the sequence of directories and jar files that make up the specspath. If no such specification file is found, any specifications in the .java source file are used, if one exists (as found on the command-line or on the sourcepath); otherwise default specifications are used in conjunction with the class file. Note that if a .jml file is found, then any specifications in the corresponding .java file are (silently) ignored. (TBD: what if the file on the command-line is not in the sourcepath?)

Last modified Nov 14 2025.