JML Tutorial - Method Selection
One way to be more efficient is to limit your attention to one file or even one method at a time. This page describes how to expand or contract the set of methods being verified.
Files and Folders
First, remember that the OpenJML
command-line lists options (and their values) and files,
just like the Java compiler (javac
) does. Usually though you have a set of interdependent files
together in one folder. So OpenJML
allows you to put a folder path on the command-line,
after the --dir
option, as in openjml --esc --dir ~/myfiles
. You can use the --dirs
option
to list several files: openjml --esc --dirs ~/myfiles1 ~/myfiles2 ~/myfiles3
. Listing a
folder name includes subfolders recursively by default. If you don’t want recursion, then list
the files using a wildcard as in ~/myfiles/*.java
. The --dirs
option interprets all
successive command-line arguments as folder paths, up to an argument that begins with a hyphen (-
).
Specific methods
To limit proof attempts to specific methods, use the --method
and --exclude
options.
- By far the most common use is
--method=<name>
, where<name>
is a simple name of a method. Then, within all the files (and folders) listed on the command-line, any method with that name is (attempted to be) verified. You can exclude everything with a given name using--exclude
. Both of these options can take multiple comma-separated names.--exclude
takes precedence over--method
. A constructor is named the same as its parent class. - A simple name can be ambiguous. To resolve ambiguity, use a full signature: either or both
a prepended fully-qualified class name or an appended argument signature, as in
--method="mypackage.MyClass.myMethod"
or--method="myMethod(int,java.lang.String)"
. Note that when the expanded name includes characters interpreted by the shell, such as periods and parentheses, quotes around the method name are needed. - More complicated strings that include wildcards for matching are described in the Ope JML Users’ Guide.