When the user launches the Spec Validator, the tool displays its initial interface, as shown in Figure 1.

Once a specification is loaded, the user enters the name of an operation to be tested in the 'Operation' text field. To do so, the user types the full name of an operation, or an unambiguous leading prefix for an operation name. When the user presses the TAB or ENTER key, the tool locates the operation in the current specification, and completes the entry in the 'Operation' text field. The completion is the full spelling of the operation name, and the operation input/output signature. If an operation name is overloaded in the specification, the user can disambiguate by typing one or more input argument types.

As an alternative to typing the operation name, the user may press the 'Browse' button next to the text field. When the user does so, the tool displays an alphabetic list of operation names, from which the user can select.

When an operation is selected, the tool displays its precondition and postcondition expressions in the two text areas immediately below the 'Operation' field. If the operation specification has a description, the tool displays it in the so-labeled text area.

The 'Operation' field, and the three text areas below it are all user editable. If the user discovers that changes need to be made to any of the information in these texts, the user may perform the edits and save the changes.

The 'Test Plan' edit area is the primary focus of the interface. It is where the user enters test cases to be used to validate the logic of the precondition and postcondition. Upcoming examples illustrate the details of defining these test cases.

The eight buttons on the bottom of the display perform the following actions:

• 'Load Spec' provides a file chooser dialog in which the user selects a specification file to load.
• 'Load Tests' provides a file chooser dialog in which the user selects a previously-saved testing file.
• The 'Save' button saves any changes the user has made, to the specification and/or test plan; specification changes are saved in the most- recently loaded specification file; test plan changes are saved in the loaded test file, or in a file of the user's choice if no test file has yet been loaded.
• 'New Case' opens a test-case editing dialog in which the user enters the details of a test case
• The 'Edit Case' button is enabled when the user selects an existing test case in one of the rows of the Test Plan; when the user makes such a selection, pressing New Case opens the test-case editing dialog on the selected test case.
• The 'Delete Case' button is enabled when the user selects an existing test case in one of the rows of the Test Plan; when the user makes such a selection, pressing Delete Case removes that test case from the plan.
• The 'Validate Case' button is enabled when the user selects an existing test case in one of the rows of the Test Plan; when the user makes such a selection, pressing Validate Case performs the validating evaluations on that one case
• 'Validate All' performs the validating evaluation on all cases of the test plan.