Prover Options

  

Clicking Prover Options invokes a window of several more options, entitled Select an Operation . We discuss each of these here. The actual prover options will be described in a subsequent sections.  

Use Default Specware Proof Options.

   Selecting this means the settings of the theorem prover will revert to the default. This may be necessary if the user has altered the options since starting to run Specware, and wishes to go back to the original settings.

Display/modify Specware Proof Options.

  This choice will postpone the setting of the proof options until the first time the theorem prover is called. At that time a menu of proof options will be displayed and settings can be edited with the mouse. Those settings will be retained for subsequent invocations of the theorem prover--the menu options will not be displayed again.

Set Specware Proof Options.

  Selecting this enables the user to alter the strategic settings of the theorem prover at once. The current settings, which have been set by default or created previously by the user, will be displayed. The user may mouse-edit those settings that need to be changed.   The options are described in a later section ().

Set Prover Display Options.

  Selecting this enables the user to alter the way the theorem prover displays the record of its proof attempts. The options will be described in a later section ().

Set Problem-set Directory

  Selecting this enables the user to alter the location in which   completed proofs are saved. Proofs will be dumped into a directory for which a default is displayed, currently /specware/2-0-1/code/prover/kitp/problem-set/. The user must accept the default or provide an alternative.  

• Set Specware Proof Options
• Set Prover Display Options