Interaction

All the interaction between the user and Specware takes place through the Lisp shell. The .sw files that define units are edited outside of Specware, i.e. using XEmacs, Notepad or any other text editor of choice. These files are processed by Specware by giving suitable commands at the Lisp shell.

When .sw files are processed by Specware, progress and error messages are displayed in the XEmacs buffer containing the Lisp shell. In addition, the results of processing are saved into an internal cache that Specware maintains. Lastly, processing of certain kinds of units result in new files being created. For example, when Lisp code is generated from a spec, the code is deposited into a .lisp file.

Specware also features auxiliary commands to display information about units, inspect and clear the internal cache, and inspect and change an environment variable that determines how unit identifiers are resolved to .sw files.