CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

### Homework Assignment

#### Instructions:

1. Copy PVS source files E.pvs and F.pvs into your working directory.
2. Prove all theorems in both files.
3. Turn in .prf and .status as usual.

#### Notes and Hints:

• The PVS source files contain additional instructions and hints. The PVS decision procedures can solve all arithmetic subgoals, once you have set them up properly.

• E.pvs:
• The proofs make extensive use of the TYPEPRED prover command, which is the main point of the exercise. TYPEPRED is used to bring typing information into a proof sequent. This information is often declared using predicative type declarations, as is illustrated in the example.
• The idea is to get all the necessary information into the sequent, flatten the logic, and then use SIMPLIFY or ASSERT to finish the proof. Remember that you should always try to use the simplest command (e.g. SIMPLIFY) that performs the task. If you are absolutely comfortable with flattening all the logic and ASSERTing away the arithmetic, you are ready to use GROUND. Enter M-x help-pvs-prover-command and ground so see what it does.
• Once you prove all the theorems in the file, the E.status file may (will) look like this:
 ``` Proof summary for theory th_E proj_TCC1.............................unfinished [SHOSTAK]( n/a s) budget_TCC1...........................unfinished [SHOSTAK]( n/a s) cost_TCC1.............................unfinished [SHOSTAK]( n/a s) E_1...................................proved - incomplete [SHOSTAK](1.38 s) E_2...................................proved - incomplete [SHOSTAK](0.72 s) E_3a..................................proved - incomplete [SHOSTAK](0.71 s) E_3b..................................proved - incomplete [SHOSTAK](0.27 s) E_3c..................................proved - incomplete [SHOSTAK](0.62 s) E_4...................................proved - incomplete [SHOSTAK](0.06 s) E_5a..................................proved - incomplete [SHOSTAK](0.07 s) E_5b..................................proved - incomplete [SHOSTAK](0.31 s) E_5c..................................proved - incomplete [SHOSTAK](0.59 s) E_6a..................................proved - incomplete [SHOSTAK](0.03 s) E_6b..................................proved - incomplete [SHOSTAK](0.03 s) E_6c..................................proved - incomplete [SHOSTAK](0.09 s) Theory totals: 15 formulas, 15 attempted, 12 succeeded (4.88 s) Grand Totals: 15 proofs, 15 attempted, 12 succeeded (4.88 s) ```
The unfinished items, prog_TCC1, etc., will be explained in lecture. At this point, you are not expected to prove them (or find them, for that matter).

• F.pvs:
• In addition to commands you have already seen, proofs require the use of (INDUCT v), for induction over variable v.
• Hint: If ASSERT doesn't work when you think it should, look for something to EXPAND.