</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> </i></font> </table> <H3> Homework Assignment </H3> <b>Instructions:</b> <ol> <p> <li>Add PVS source files <font color="green"<tt><b><a href="C.pvs">C.pvs</a></b></tt></font> and <font color="green"<tt><b><a href="D.pvs">D.pvs</a></b></tt></font> to subdirectory <font color="blue"><tt><b>class/<i>student_id</i>/2</b></tt></font> of your homework directory. <li>Using PVS, prove the theorems in each file and generate status files <font color="darkgreen"<tt><b>C.status</b></tt></font> and <font color="darkgreen"<tt><b>D.status</b></tt></font> <li><b>Note:</b> The last result in <font color="green"<tt><b><a href="D.pvs">D.pvs</a></b></tt></font>, <tt>THEOREM D_10</tt>, is <i>optional</i>; in fact, you will be unable to complete its proof using the commands we have seen so far, but it is worthwhile to try. <li>Deposit all <font color="green"<tt><b>*.status</b></tt></font>, <font color="green"<tt><b>*.prf</b></tt></font>, and <font color="green"<tt><b>*.pvs</b></tt></font> files to your SVN directory. </ol> <p> <h4>Notes and Hints:</h4> <ul> <li>The PVS source files contain additional instructions. <ul> <li> In <font color="green"<tt><b><a href="C.pvs">C.pvs</a></b></tt></font>, you are to use <em>only</em> <font color="red"><tt><b>SPLIT</b></tt></font>, <font color="red"><tt><b>FLATTEN</b></tt></font>, <font color="red"><tt><b>INST</b></tt></font>, <font color="red"><tt><b>SKOLEM</b></tt></font>, <font color="red"><tt><b>LEMMA</b></tt></font>, <font color="red"><tt><b>SIMPLIFY</b></tt></font>, and <font color="red"><tt><b>ASSERT</b></tt></font>. <li> In <font color="green"<tt><b><a href="D.pvs">D.pvs</a></b></tt></font>, you will need need <font color="red"><tt><b>EXPAND</b></tt></font> and <font color="red"><tt><b>REPLACE</b></tt></font> in addition to the commands above. <li> Try <font color="red"><tt><b>SIMPLIFY</b></tt></font> before using <font color="red"><tt><b>ASSERT</b></tt></font>. </ul> <li> <font color="green"<tt><b><a href="C.pvs">C.pvs</a></b></tt></font> <ul> <li> I recommend that you first solve the problem on paper, without referring to the axioms and lemmas in the file. <i>Keep notes on <u>how</u> solved it.</i> <li> Then read through the file to see how the solution is <em>formulated</em> in PVS and how this formulation compares with with your solution. <li> Now, prove the theorems. You may prove them in any order you wish, but doing the proofs in order is recommended. <li> You might be interested in the <i>solution method</i> <a href="C_solution.pdf">[PDF]</a> you were taught in your first pre-algebra class. </ul> <li> <font color="green"<tt><b><a href="D.pvs">D.pvs</a></b></tt></font> <ul> <li> Write pencil-and-paper proofs for a few of the theorems before attempting them in PVS. <li> Compare the PVS proof in <font color="green"<tt><b>D.prf</b></tt></font> with your written proof. What PVS proof commands, if any, are reflected in an English proof narrative? </ul> </body> </html>