</head> <BODY vlink="#990099" link ="#990099", alink="#990099"> <table noborder cellpadding=0 cellspacing=0 width="100%"> <tr bgcolor="#EECCFF"> <td width="50%" align="left"> <font size=-1><i> <a href="http://www.cs.indiana.edu/classes/p415-sjoh/">CSCI P545</a> </i></font> <td width="50%" align="right"> <font size=-1><i> Sat Jan 24 11:14:37 EST 2009 © <a href="http://www.cs.indiana.edu/~sjohnson">[SDJ]</a> </i></font> </table> <H3> Homework Assignment </H3> <h4>Instructions:</h4> <ol> <li> Copy PVS source files <font color="green"><tt><b><a href="E.pvs">E.pvs</a></b></tt></font> and <font color="green"><tt><b><a href="F.pvs">F.pvs</a></b></tt></font> into your working directory. <li> Prove all theorems in both files. <li> Turn in <font color="green"><tt><b>.prf</a></b></tt></font> and <font color="green"><tt><b>.status</a></b></tt></font> as usual. </ol> <p> <h4>Notes and Hints:</h4> <ul> <li>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. <li> For <font color="green"><tt><b><a href="E.pvs">E.pvs</a></b></tt></font>: <ul> <li> The proofs make extensive use of the <font color="red"><b><tt>TYPEPRED</tt></b></font> prover command, which is the main point of the exercise. <font color="red"><b><tt>TYPEPRED</tt></b></font> is used to bring typing information into a proof sequent. This information is often declared using <i>predicative type</i> declarations, as is illustrated in the example. <li> The idea is to get all the necessary information into the sequent and then use either <font color="red"><b><tt>GROUND</tt></b></font> or <font color="red"><b><tt>ASSERT</tt></b></font> to finish the proof. Like <font color="red"><b><tt>PROP</tt></b></font>, <font color="red"><b><tt>GROUND</tt></b></font> eliminates <i>all</i> the logic operators. After that, <font color="red"><b><tt>ASSERT</tt></b></font> is applied to each of the resulting subgoals. So while the instructions in the file say to try <font color="red"><b><tt>GROUND</tt></b></font> first, I would recomment trying <font color="red"><b><tt>ASSERT</tt></b></font> first. <li> Once you prove all the theorems in the file, the <tt><b>C.status</b></tt> file may (will) look like this: <blockquote><table border><tr bgcolor="#FFFFEE"><td><pre> 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) </table></blockquote> The unfinished items, <tt><b>prog_TCC1</b></tt>, etc., will be explained in lecture. At this point, you are not expected to prove them (or find them, for that matter). </ul> <li> <font color="green"><tt><b><a href="F.pvs">F.pvs</a></b></tt></font>: <ul> <li> In addition to commands you have already seen, proofs require the use of <font color="red"><b><tt>(INDUCT <i>v</i>)</tt></b></font>, for induction over variable <font color="red"><b><tt><i>v</i></tt></b></font>. <li> <i>Hint:</i> If <font color="red"><b><tt>ASSERT</tt></b></font> doesn't work when you think it should, look for something to <font color="red"><b><tt>EXPAND</tt></b></font>. <ul> </ul> </body> </html>