Specware is a development environment that runs on top of Lisp. The following sections describe the Specware environment and the basic mechanisms for running Specware.
The user interacts with Specware through the "Specware Shell", with the choice of running the latter in an XEmacs buffer or in a Lisp window. XEmacs users will almost certainly be more comfortable with the first choice, while the second choice may be preferable for users unfamiliar with Xemacs.
To start Specware, double-click either the Specware4 XEmacs shortcut or the Specware4 shortcut on your Desktop, or select one of the two from the Start Menu -> Program Files -> Specware menu.
When Specware is launched through the Specware4 XEmacs shortcut, a couple of things happen: an Allegro Common Lisp Console window appears (which may be ignored but should not be closed), XEmacs is started, and a Lisp image containing the Specware Shell is started inside an XEmacs buffer entitled Specware Shell.
When Specware is launched through the Specware4 shortcut, a Lisp window entitled Specware Shell appears in which the Specware Shell is running.
In either case, the Specware Shell starts with issuing a prompt (an asterisk "*"), prompting the user to issue a Specware Shell command. All of the user interaction (see the next chapter) with Specware occurs at the Specware Shell prompt: the user issues a command; Specware processes it and shows any results or error messages, insofar as applicable; then prompts the user; and so on, until the end of the session.
Processing errors may cause the execution of the Specware Shell to be interrupted, throwing interaction into a Lisp shell. To return to the Specware Shell, issue the Lisp command :sw-shell. Alternatively, select an appropriate restart action if one is offered by Lisp.