Customize

   Clicking Customize invokes a menu window of several more options, entitled Set SPECWARE Parameters . The current settings are the alternatives highlighted in reverse. If no settings have been changed, the defaults are presented. We discuss those options that apply to theorem proving here.

Verify parsed theorems?

 Clicking Yes indicates that we want to prove theorems that occur explicitly in a specification that is being parsed. Otherwise, the specification will be parsed without invoking the theorem prover, but it can be verified later (see ) . The default is No.

Verify parsed axiom translation?

     Clicking Yes indicates that when a morphism is parsed, we want to prove that the axioms of the source specification do indeed map into theorems of the target specification. Otherwise, the morphism will be parsed without theorem proving, but the theorems can still be verified later  (see ). The default is No.

Assume imported conjectures are theorems?

   In building an axiom list  from a specification that imports   another specification, click Yes if you want theorems from the imported specification to be assumed without proof, and No if you don't want to assume them. In this later case, the imported conjectures will be ignored if we are parsing; if we are verifying the specification subsequently (see ), we will be offered the opportunity to prove the imported conjectures. The default is Yes.

The choice of a subset of conjectures is described subsequently ().   

Assume preceding local conjectures are theorems?

  Clicking Yes causes previous conjectures  in a specification to be added to the axiom list  and temporarily regarded as valid, whether or not they have actually been proved. Clicking No means they won't be added to the axiom list unless they have been proved previously. These selections also apply to previous translations of axioms in a morphism . The default is No.

Ignore following local theorems when proving a conjecture?

  Yes means that subsequent conjectures  in a specification will not be included in the axiom list, even if they have already been proved. Clicking No means they will be added to the axiom list if they have been proved previously. These selections also apply to morphisms . Note that the user who assumes preceding local conjectures are theorems (the previous option) and does not ignore following local theorems is opening the door to circularity : it could happen that the proof of the subsequent theorem depended on an assumption that the current conjecture is a theorem.

Select Conjectures to verify?

    Clicking No will cause all the conjectures that arise in a parsing to be treated as a single batch and attacked with the same strategic settings.  Clicking Yes will enable the user to select a subset of the conjectures to be treated as a batch and attacked with the same settings; other conjectures may then be batched separately and attacked with different settings. The default is No.

In a later section (), we see how conjectures are selected.

Specify proof directives for?

  Here the user is given three options, not Yes or No. Clicking Every-Batch means that the user will be allowed to select separate strategic settings for every batch of conjectures formed in accordance with the earlier option, Select Conjectures to verify? Clicking Every-Proof means that separate strategic settings may be selected for every proof. Clicking None means that no strategic settings may be selected--the most recent settings will be retained in every proof. The default is None.

When prover fails, query user to accept theorems anyway?

    Yes--the default--means that if a proof fails, the user will be given the opportunity to accept the conjecture as valid. It will subsequently be regarded as a theorem and will be included in the axiom lists for subsequent proofs. Clicking No means the proof will fail, the conjecture will not be regarded as a theorem, but the parsing of the specification or morphism will continue.

In a later section (), we see how proof directives are specified.

• Select Conjectures to Verify?
• Specify Proof Directives
• Specify Proof Tactic
• Specify theorem usage as default