Sample Sessions

   In this section we give sample sessions involving the use of the theorem prover. We use examples from the specifications we have seen in an earlier Section ().

Before exercising the theorem prover, we select Customize from the Specware toolbar. The menu Set SPECWARE Parameters (see ) appears. We select

Verify parsed theorems? Yes

Verify parsed axiom translation? Yes

Select conjectures to verify? Yes

Specify proof directives for: Every Batch

Although this specification has only one conjecture, we shall use these settings also for subsequent specifications, which have more than one conjecture. All other items remain with the default settings. Then we select Do It.

We then select Prover Options from the Specware toolbar. The menu Select an Operation appears. We choose Set Specware Proof Options. A new menu, Set New Values for Prover (Kitp) Parameters appears (see ). We leave all the settings with the default, except

Include Sort Axioms? No

As soon as we select Do It, another menu appears, Set Prover Display Options (see ). We alter the following items:

Suppress KITP Message? No

Display Proof Object Both

Display Input Clauses Yes

Display Forward Derivation? Yes

Display Backward Derivation? Yes

Whereas normally the theorem proving is relatively invisible, we have selected options that provide us with more information.

We then parse the specification COLLECTION  that we saw earlier (). A copy of this specification, and others, appears on the Specware file /specware/2-1-a/library/slang-specs/examples/collection.re.

The specification contains only one conjecture, the decomposition  theorem. Because we have asked to treat conjectures in separate batches, we are presented with a menu containing only this conjecture (see ). We select it (or the option All of the Above) and then Do It.

We are presented with another menu, Specify Proof Directives for Spec COLLECTION (see ). We select

Specify induction tactics? Yes

Specify prover usage of Spec axioms/theorems: \

Rewrite Forward Backward Left-To-Right Right-To-Left

Set KITP prover options? No

We then select Do It. We have chosen all the options for prover usage--this means that we will be offered all these options for each axiom in the axiom list.

Next we are given the menu Specify Proof Tactic (see ). This gives us the chance to decide whether we want to use the induction tactic in proving our conjecture. In fact, the proof does require induction, but suppose we try it without induction; we select None followed by Do It.

We are presented with the menu Proof failed. Choose a return value: We select False, because we do not want the result to be accepted without proof.

Similarly, when presented with the menu Accept conjecture Decomposition (shown in *REFINE* window) as verified anyway?, we select No.

We are presented with an option Verify the remaining unverified conjectures?. In this case, there is only one conjecture, the one we have just failed to prove. We select Yes.

We repeat the process starting with the menu Select conjectures to prove, only this time we choose Yes when asked Specify induction tactics? (see ).

When given the menu Specify Proof Tactic (see ), we chose Ind: C, (INSERT-COL, EMPTY-COL). This is the only alternative offered here for an induction proof; it indicates that induction will be on c, and specifies the constructor set.

This time, the proof is successful. To do the proof by induction, the inductive tactic actually divides the conjecture into two parts, a base case and an inductive step. The inductive step is performed first. KITP succeeds on both parts, and reports the proof of each part, as we have requested.