Extended Static Checking for Java - V2 - GUI application

The ESC/Java2 tool is an updated version of ESC/Java. It is consistent with Java 1.4 and with the current version of JML. It is available as a Java release and there is additional information about how to use Esc/Java2 and JML in that release. The documentation page that you are now reading describes a GUI tool that contains ESC/Java2, providing a convenient graphical interface as an alternative to the command-line application. Though you can try this tool as it is, full use of it will require familiarity with static checking using Esc/Java2 and its parent, Esc/Java.

Table of Contents


Starting the tool
Organization of the tool
Projects
Quick start
Details of a project
Static checking
Reviewing the results
Static Checking Actions
ESC Options
GUI Options

Starting the tool

The Esc/Java2 GUI tool is shipped as a double-clickable jar file named esctools2.jar. Thus it can be launched either
  • (a) by double-clicking the file (on most platforms), or
  • (b) by issuing the command-line command "java -jar esctools2.jar" or
  • (c) by issuing the command-line command "java -classpath esctools2.jar escjava.gui.GUI", or
  • (d) if you are working from a Esc/Java2 development environment or release, with the command "escjava -gui" .
With options (b), (c) and (d), additional command-line arguments may be appended as well.

Typechecking can be performed with this tool alone, but any static checking requires in addition a copy of the Simplify executable appropriate for the platform. There are versions of Simplify available in the Esc/Java2 release for Mac OS X, Windows, Linux, and Solaris platforms.

Organization of the UI

The UI has the following pieces:
  • a menubar across the top of the window or the top of the screen;
  • a number of buttons that provide easy access to some of the menubar functionality;
  • a status area;
  • a main panel with 4 tabs:
    • a tab, "GUI Options", that allows the setting of options that control the GUI tool itself (these are not saved as part of a project);
    • a tab, "ESC Options", that allows the setting of options that control the running of the ESC/Java2 tool;
    • a tab, "Project files", in which classpaths and input files are listed;
    • a tab, "Results", that allows initiating and reviewing the results of the static checking operations.
  • The results panel itself has these elements:
    • a panel showing a tree structure of the compilation units, types and routines contained in the input files;
    • a free-floating error message window (not initially shown);
    • a free-floating rudimentary source code display and editor window (not initially shown).
  • Most GUI elements also have tooltips that provide information about the purpose of that element.
  • The "Help" menu has a menu item brings up this help document.

Projects

The tool allows work to be organized into projects. A project contains the options, classpath definitions, and list of the files, directories, packages, classes, or list files to be acted upon. It is the same material as would be specified on the command-line. Project information can be saved into project files and reloaded from project files. Project files do not contain the results of the tool, only the input material. The tool operates only on a single project at a time.

The tool begins with a default project. All options are set to default values, the classpath is obtained from the environment, and the list of input files is empty. Thus to begin work, you first have to add some content to the project. You do this on the "Project Files" tab.

Projects can be saved in and loaded from project files. You can also use project files from the command-line using the -f option.

Quick start

Step 1: Launch the tool by double-clicking the jar file, or by issuing the command "java -jar esctools2.jar" from the command-line.

Step 2: Click on the tab for the "ESC Options". Enter into the text field labeled "Path to Simplify executable" the absolute path of the executable appropriate for this platform. You may use the "Browse" button to find the executable using a graphical directory navigator, if you like.

Step 3: Click on the tab for "Project files". Type into the text area, on a single line, the path to a file containing the code to be checked. If you need to adjust the CLASSPATH do so as well. Multiple files may be listed, one per line. You may also give the path to a directory or the fully-qualified name of a package or class.

Step 4: Click on the tab for "Result". The name of the input file should be present in the Results Pane. Click the "Check" button. The results tree will expand to show the types and routine names found in the input file. The will be colored green if the various checks pass successfully. If not, the nodes will be colored red and a text window will appear containing error messages.

Step 5: To analyze the results, hold down the ALT key and click on any node in the tree that is colored red. This will bring up a scrollable text window containing the messages generated by checking that item. If a line in that window contains a filename and a line number, you can click on the line to bring up an editor window for that file with the offending line selected and viewable in the scrollable editor window. Changes made there can be saved back to the file by pressing the Save button. [ In order for the changes to have an effect on the checking, you must reload the input files by pressing the Reload button. ]

Details of a project

Input files: The tool operates on a set of input files, directories, packages, classes or filelists. These are listed one per line within the input file text area.

Files and directories are listed by name in the manner defined for the platform on which the tool is running; they are found relative to the working directory of the shell in which the application was launched. Listing a directory is equivalent to listing all the files in that directory that have active JML suffixes (.java, .jml, .spec, .refines-java, .refines-spec, .refines-jml).

If a package name is listed it is looked for on the sourcepath (rather than the working directory), and results in the tool operating on all JML files in that package. Similary, a fully-qualified class name is found on the sourcepath.

A filelist is a text file that contains the names of files, directories, packages or other filelists, listed one per line.

White space before and after directory names is ignored; file and directory names may be enclosed in quotes if they have internal white space.

The application interprets a given name as a file, directory, list, package or class as best it can. The user may help to disambiguate these by prefixing the name on the same line with one of -file, -dir, -package, -class, or -list.

Classpath text field: The classpath is used to find any .class files for classes contained in or referenced by the input files (and for all .java and specification files if there is no sourcepath). By default, the classpath value is taken from the environment (the CLASSPATH environment variable). If that is not defined the value will be just the working directory. The classpath (and sourcepath) is a sequence of directories separated by a platform-dependent separator character (typically either a colon or semi-colon); be sure to use the correct character for your platform.

Specpath text field: The specpath is a directory path containing specification files for system classes. This would typically include specifications for classes shipped with a Java implementation (e.g. for java.lang.String), but might also include specifications for other class libraries you use. The jar file that contains the application also contains a set of specification files, so the default setting of the specpath is to the jar file from which the application is launched.

Static checking

There are four phases to the checking of the input.

  • Resolving input names. Each input item is interpreted as a filename, a directory, a package, a class or a list. Each input item can be prefaced by one of the option keywords -file, -dir, -package, -class, or -list to indicate which kind of input it is. An input without one of these is interpreted first as a file if a file with that name (or path) exists, as a directory if a directory with that name or path exists, then as a package or class. A file that is a list must be prefaced by the -list keyword. Each input is expanded into the set of jml-relevant files that it contains.
  • Parsing a file. Each file generated by the above is read and parsed. In doing so other files in the compilation unit's refinement sequence are also read, but no reference is made to any of the classes that are referenced in the input file. The result is a composite parsed compilation unit. Syntax errors will cause this phase to partially or completely fail.
  • Typechecking. Each class and routine in a compilation unit is then checked to be sure it is well-formed. In the process, any type names in the compilation unit are resolved: their type declarations are found from the directories specified in the sourcepath and classpath. Consequently, additional files may be parsed and typechecked. Errors such as missing type definitions, expressions that have the wrong type or semantic errors such as misusing a static declaration of a member of a type can cause this phase to fail. Typechecking currently cannot be performed incrementally, since the checking of one class is dependent on many others. Thus if the project settings or the set of input files are changed, all typechecking must be redone.
  • Static checking. In this phase, verification conditions are created for each class and routine and sent to the prover subsystem for checking. Code that appears to violate the specifications, according to the prover, results in "warnings" being issued. The checking of a given routine may depend on the specifications of many other classes and routines. The static checker can operate on each routine individually, presuming all relevant classes have typechecked successfully.

Reviewing the results

There are three tools for reviewing the results of static checking.

The tree of input elements

The results pane shows the list of input elements (files, directories, packages, etc.). Once the input element has been resolved into the list of files contained in it, those files are shown as the next level of nesting. If the file is parsed successfully (including the other files in the refinement sequence), then the next two levels of nesting will show the classes and the routines contained in the parent compilation unit.

The tree of compilation units, classes, and routines is color-coded. The background color for each tree node indicates the errors produced.

  • White: The item has not been processed.
  • Red: An error or static checker warning occurred in processing.
  • Green: All checks passed.
  • Yellow: Some cautions were generated, but no errors or warnings.
  • Orange: Some child nodes have errors (useful if the tree is collapsed, to know about hidden children with errors).
  • Blue: The static checker timed out or the verification condition was too large.

The error window

As each routine is checked, if there are warnings or errors or cautions produced, an output window is generated that contains the text of the corresponding messages. This is produced for any of the parsing, typechecking or static checking phases that have errors. Thus there is displayable output for any node that is marked as having not passed its checks. The output window is scrollable and the output messages contain the file name and line numbers of the offending statements. You can display the output of any node by ALT-clicking on the node label in the results tree or by selecting the node and then activating the "Error Window" menu item under the "View" menu.

An editor window can be launched for a compilation unit, a class, a routine, or an error message. This brings up a very rudimentary editor, positioned at the appropriate line number. Minor edits can be performed and the result saved back to the file system. Changes that are not saved (or not yet saved) are not used in static checking; the checker always reads from the file system. Those saved are only used after the tool has "Reloaded" the input. You can bring up an editor window by either

  • clicking on a line in the error window that contains a file name and a line number (this will scroll the window to the specified line), or
  • selecting a file, class, or routine in the results tree and then selecting the View->Editor menu item from the menu bar, or
  • selecting a file, class, or routine node in the results tree while holding down the CONTROL key.

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...