Static Checking Actions
This section is a reference to all the GUI operations (menus, buttons,
accelerator keys,...) that can be performed by the tool. Details of
the two option panes are given in succeeding sections.
Window actions
Close window: (Clicking the X in the upper right on Windows,
the red button in the upper left on Mac). This action terminates the
program. There is no confirmation dialog, even if you have loaded and
altered a project.
Question: TBD - should it ask to save the current project?
Other window operations: Other generic window operations have
the same effect as for other windows on that platform.
File menu
New Project: This action will delete the current project
(but not the project file or any other file associated with the project)
from the tool and initialize to a default, empty project. There is no
confirmation dialog that you want to forget that current project. It does
not reset any GUI or ESC options.
Question: TBD - should it ask to save the current project?
Open Project: This action will launch a file browser enabling
the user to choose a new project file to load. There is no
confirmation dialog that you want to forget the current project. The file
browser begins in the current working directory, but subsequent uses of the
file browser begin in the directory where it was last left. Loading a new
project will change the ESC Options as well as the classpaths and input list
to the values recorded in the project file.
Save Project: This action will save the current project
in the same file from which it was loaded. If there is no source file
(since the project is a modification of a default project), then this
button will provoke the same action as "SaveAs Project". There is no
confirmation that you do indeed want to save the new state of the project.
SaveAs Project: This action will launch a file browser enabling
the user to choose a directory and file name under which to save the
current project. There is a confirmation dialog that asks if you want to
overwrite an existing file, should you choose one. The same file browser is
used as in the "Open Project" browser, and thus repeated uses of SaveAs will
start the file browser in the directory where the previous one ended.
Close (on non-Mac platforms): Exits the program without any confirmation
dialogs.
View menu
Error window: Launches a window displaying any output text corresponding to any
selected nodes in the results tree. Silently does nothing if nothing is selected.
Editor window: Launches an editor window for any files or routines that are selected
in the results tree. For selected routines, the window will scroll to the region of the
routine declaration. Silently does nothing if nothing is selected.
Check menu
Check All: Begins a full set of checks on all the input. Items that are already
checked are not re-checked.
Check Selected: Begins a full set of checks on each selected node and its children. Items that are already
checked are not re-checked.
TypeCheck All: Performs typechecking but not static-checking on all the input. Items that are already
typechecked are not re-checked.
TypeCheck Selected: Performs typechecking but not static-checking on each selected node and its children. Items that are already
typechecked are not re-checked.
Parse All: Performs parsing but not type- or static-checking on all the input. Items that are already
parsed are skipped.
Parse Selected: Performs parsing but not type- or static-checking on each selected node and its children. Items that are already
parsed are skipped.
Resolve All: Converts all input items into the set of implied files. Items that are already
resolved are skipped.
Resolve Selected: Performs parsing but not type- or static-checking on each selected node and its children. Items that are already
resolved are skipped.
Clear All: Clears away all results of static checking. This is useful if you want to
rerun static-checking with a different set of options. It does not reread the input files
or redo any resolving, parsing or typechecking.
Clear Selected: Clears away all results of static checking for selected nodes and their children. This is useful if you want to
rerun static-checking with a different set of options. It does not reread the input files.
Tools menu
Gen. Skeleton: This will eventually provide a means to generate a specification
skeleton, but is not yet implemented.
Garbage Collect: Initiates garbage collection. Note that the status bar shows the
current memory consumed by the application.
Help menu
Documentation: Brings up a scroll-able window containing this documentation.
Issues/Bugs: Brgins up a scrollable window containing release notes about the
application, including known problems and some of the outstanding feature requests.
Buttons
Reload: Clears away the results of all name resolution, parsing, and checking, as well
as the results tree. It rereads the input list in the light of any classpath or other
changes to options, regenerating the top-level of the output tree.
Clear: Deletes the results of any static checking, but not of parsing or typechecking.
If any nodes are selected, only those nodes and their children are cleared
(equivalent to "Clear Selected"); if no nodes are selected, everything is cleared (equivalent
to "Clear All").
Check: Performs static checking, and any prerequisite name resolution, parsing or
typechecking.
If any nodes are selected, only those nodes and their children are checked
(equivalent to "Check Selected"); if no nodes are selected, everything is checked (equivalent
to "Check All").
Stop: Pressing this button cancels the current operation and any pending operations.
Some computations, particularly typechecking, may take a bit of time to halt.
Status area
The status area is below the button area and above the tabbed pane area. It consists of
two labels showing current information and two colored squares giving other status information.
Current action label: The label to the left shows the current activity (e.g. parsing,
typechecking...) and the item being acted on. If the area is blank, no processing is
happening.
Memory usage label: The label to the right show the current memory usage as
reported by calls to the runtime system. It is updated on a regular schedule.
GUI action square: The colored square on the left shows the current activity of the
GUI: Blue - waiting for a command; Green - processing in response to a command; Yellow -
waiting for a response from the prover.
Prover action square: The colored square on the right shows the current activity of the
prover: Black - not running; Blue - waiting for a command; Green - proving.
Project inputs pane
This pane (along with the ESC options pane) contains the material which is the input to the
static checker. Changes to any elements here will cause the results pane to be reloaded.
Classpath
Classpath Text Field: Enter here the CLASSPATH which is to be used to find the
classes referenced by the input files. This is not the CLASSPATH used to run the
application. The syntax is that of standard directory paths; use the separator
character appropriate to your platform. Wild-card characters and variable references
are not permitted. The data entered into the field is "accepted" by the application when
a return character is typed or when the field loses focus. Note that the field does not
necessarily lose focus when one proceeds directly from typing in the field to selecting a
menu item (such as Save).
Spec path
Spec path text field: Enter here the directory path for system specification files.
You may also include specifications for libraries that you reference by your inputs. This is
a standard directory path. The comments about data entry under CLASSPATH above are pertinent
here as well. The application jar file includes a set of JML specifications for system
classes and JML model files; thus the default Spec Path is the jar file that contains the
application.
Input list
Input text area: The large text area in the "Project Files" pane
is used for listing the input items on which static checking is to be
performed. One can edit this in a fairly freeform manner. The application
expects the input in the following form.
- One input entry per line.
- An input entry consists of an optional type designator and a name.
- The name is a name of a file, a directory, a fully-qualified package name,
a fully qualified class name, or a list file.
- Files, list files, and directories may be written either as absolute paths or
as paths relative to the working directory in which the application was launched.
- Packages and classes are found on the classpath.
- White space that preceeds or trails a file, list file or directory name is ignored,
unless the full path is enclosed in quotes (").
- A list file is an ordinary text file that contains, one per line, file, directory,
package, class or list names (but not optional type designators).
- The application will interpret each name as best it can, but the user may also provide
an optional type designator to tindicate the type of the entry.
- The type designators are
-file, -dir, -package,
-class, and -list. They must appear at the beginning of a line
of text (no preceeding white space) and be separated from the input entry name by white
space.
Results Pane
Results tree: The results pane contains a tree structure that shows the results of
checking the inputs. Initially this will just show the input elements. As checking
proceeds, four levels of the tree will be populated.
- The top level shows the input elements themselves, whether or not they are valid.
- The second level shows all the files/compilation units contained in the input element.
An input element that is a file will just contain the one file. A directory or package or
list will contain many files. After parsing, these tree nodes represent the compilation unit
obtained from the file or from the full refinement sequence that contains the given file.
- The third level shows the classes contained in a given compilation unit. Often a
compilation unit will contain just one class, but it may contain more than one.
- The last level shows the routines contained in each class.
The second level is not known until the top level has been "resolved"; the inner two levels
are not known until the second level has been "parsed". By default the tree will expand as
checking proceeds and new nodes are added, though that can be turned off on the GUI options
pane.
As checking proceeds, the nodes become color-coded. The colors have these meanings.
- White - not yet processed.
- Yellow - Cautions issued while processing. At the top level this could be because the
input entry cannot be found; at other levels this may indicate minor parsing or typechecking
issues.
- Green - Processed without problems.
- Red - Errors or staic-checker warnings produced during processing.
- Orange - Some child level has errors. This color is used so that if the tree is
collapsed, one can tell which higher nodes have hidden children with errors.
- Blue - Static checking aborted because of inadequate time or too large a verification
condition.
Nodes in the tree can be collapsed and expanded as is customary. Selections can be made
by clicking on individual nodes; selections can be extended in the manner customary for
your platform (e.g. on a Mac, a node is selected by a click, deselected by a command-click,
multiple selections are made with a command-click, and a range is selected with shift-click).
As checking proceeds, error windows may pop up. They will do so by default, but this may
be disabled on the GUI options pane. You can also request a window showing the output for
a given node by ALT-clicking the node (on a Mac this is an ALT or OPTION click; on my
Linux laptop this is ALT-CONTROL-click).
You can also obtain an error window by selecting a node (or nodes) and activating the
View->Error Window menu item.
Currently only one error output window is shown
at a time.
You can request an editor window for a source file as follows. You can select a node
(or nodes) and activate the View->Editor Window menu item. Alternatively you can
CONTROL-click on a node in the tree. Alternatively, you can click on a line in the error
window that contains a filename and line number. In each case an editor window for the
appropriate file is launched; in the latter case the window is scrolled to the neighborhood
of the designated line. Similarly, if the window is launched by choosing a class or
routine node, the window will scroll to the region of the declaration of that class or
routine.
Error output window
The error output window is a non-editable text window that shows the output text produced
when checking a given node of the tree. It can be launched as described above from the
results tree. It can be scrolled as is customary. The one customized behoavior is this:
clicking in a line containing a file name and (optional) line number will result in launching
an editor window for that file and scrolled to the indicated line. There is just one error
window that will show the text for the most recent request; the title of the window shows
the node to which the text belongs.
Editor windows
An editor window is associated with a single source file. It is launched as described above
from either the error window or the results tree. It provides very rudimentary editing
capability, but suffices for making simple changes to a specification and saving the result
to the file system.
At the top of the editor window are a few controls:
- Save button: Saves the current text to the file system.
- Reload button: Reloads the text from the file in the file system, losing any edits
that were made.
- Go To Line text field: Entering a line number in this field and typing return will
cause the window to scroll to the neighborhood of that line.
ESC Options
Not all of the options available on the command-line are available in
the GUI. Some are not relevant, some have an unknown or untested effect,
and some are too little used (and some we haven't gotten around to).
Unless indicated, the default for each option is off. Most of them
are binary valued options with simple toggles to turn them on or off.
Simplify path
The Simplify path text field must contain the path to a Simplify executable appropriate
to your platform. You can either type into the field directly or use the browser button
to open a file system browser to locate the file.
Control of input
source 1.4: When on, Java 1.4 input,
possibly including assert statements,
is presumed. If the option is off, the assert identifier is
interpreted as an ordinary identifier and not a keyword.
enableassertions: If on (requires source 1.4), then Java assert
statements
are enabled; otherwise they are ignored.
parsePlus: If on, parses annotations in '//@' and '/*@' comments,
which are normally only processed by the JML checker.
Control of output
noCautions: If on, no Caution messages are output, only warnings and
errors and fatal errors.
noSemicolonWarnings: If on, suppresses errors caused by missing
terminating semicolons (technically illegal in JML, but tolerated by
ESC/Java2).
noNotCheckedWarnings: If on, suppresses cautions about JML
language features that are not checked by the static checker.
Debugging helps
showErrorLocation: If on, then a stack dump is produced just prior to each
output message, to assist in determing the location in the code reporting
the condition.
showDesugaredSpecs: If on, outputs a desugared and denested form of
each routine's specifications.
pgc: If on, outputs the guarded commands generated for each routine.
pdsa: If on, outputs the dsa form generated for each routine.
ppvc: If on, outputs the verification conditions (as sent to the prover) generated for each routine.
Warning types
The options in the two columns on the right side of the pane designate the various
types of warnings that the static checker checks. All except 'DeadLock' are on by
default. Turning these off is equivalent to using the '-nowarn' option on the command-line.
The documentation of ESC/Java2 provides information about each kind of warning.
Disable All button: This turns off all warning types (resulting in no static checking
at all).
Enable All button: This enables all of the warning types.
GUI Options
Auto Expand the nodes: When enabled (which it is by default), then as nodes are
added to the result tree, they are expanded, showing their children.
Auto scroll: When enabled (which it is by default), then as processing proceeds,
the result tree pane scrolls to keep the nodes currently being acted upon in view.
Breadth first checking: When enabled, then processing proceeds by first doing all
input entry resolution, then all parsing, then all typechecking, then all static checking,
processing all designated nodes at each phase. When disabled (depth first checking), then
each node in turn is processed fully to the degree requested (e.g. each node in turn will be
fully static-checked, before moving on to other nodes).
Show error windows automatically: When enabled (which it is by default), then as
nodes are processed, if there is output text, an output window is automatically produced and
made visible.
Command-line Options
TBD...