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,
--dir option, as in
openjml --esc --dir ~/myfiles. You can use the
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
--dirs option interprets all
successive command-line arguments as folder paths, up to an argument that begins with a hyphen (
To limit proof attempts to specific methods, use the
- By far the most common use is
<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.
--excludetakes 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="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.