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:
sourcepath: The OpenJML sourcepath is set using one of these alternatives, in priority order:
specspath: The OpenJML specifications path is set using one of these alternatives, in priority order:
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:
.javafile, 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.
.jmlsuffix, 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
.javasource 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?)