📄 page_476.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd"> <html> <head> <title>page_476</title> <link rel="stylesheet" href="reset.css" type="text/css" media="all"> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> </head> <body> <table summary="top nav" border="0" width="100%"> <tr> <td align="left" width="30%" style="background: #EEF3E2"><a style="color: blue; font-size: 120%; font-weight: bold; text-decoration: none; font-family: verdana;" href="page_475.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_476</strong></td> <td align="right" width="30%" style="background: #EEF3E2"><a style="color: blue; font-size: 120%; font-weight: bold; text-decoration: none; font-family: verdana;" href="page_477.html">next page ></a></td> </tr> <tr> <td align="left" colspan="3" style="background: #ffffff; padding: 20px;"> <table border="0" width="100%" cellpadding="0"><tr><td align="center"> <table border="0" cellpadding="2" cellspacing="0" width="100%"><tr><td align="left"></td> <td align="right"></td> </tr></table></td></tr><tr><td align="left"><p></p><table border="0" cellspacing="0" cellpadding="0" width="100%"><tr><td align="right"><font face="Times New Roman, Times, Serif" size="2" color="#FF0000">Page 476</font></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Courier New, Courier, Mono New, Courier, Mono" size="2">聽聽聽聽sum聽=聽sum聽+聽count;<br />聽聽聽聽count++;<br /><br />聽聽聽聽聽聽聽聽//聽Invariant:<br />聽聽聽聽聽聽聽聽//聽聽聽聽聽sum聽==聽1聽+聽2聽+聽聽+聽count-1<br />聽聽聽聽聽聽聽聽//聽聽&&聽2聽<=聽count聽<=聽11<br /><br />}聽while聽(count聽<=聽10)聽;<br /><br />//聽Assert:<br />//聽聽聽聽聽sum聽==聽1聽+聽2聽+聽聽+聽10<br />//聽聽&&聽count聽==聽11</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">The first time control reaches the position of the loop invariant, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> equals 1 and </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> equals 2. Therefore, the invariant is true. (Notice that </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> equals the sum of the integers from 1 up through 1there's just one number in this sum.) At the end of the second iteration, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> equals 3 (that is, 1+2) and </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> equals 3, so the invariant is again true. At the end of the tenth iteration, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> contains the sum of 1 through 10 and </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> equals 11. The invariant is still true. At this time, control exits the loop. Now let's verify that</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">Invariant AND Termination condition</font><font face="Symbol" size="3">(r)</font><font face="Times New Roman, Times, Serif" size="3"> Postcondition</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">(Remember that the right arrow, pronounced <i>implies,</i> is the logical implication operator.) We manipulate the assertions as follows. The loop invariant is</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> = 1 + 2 + + </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3">-1) AND (2</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3"><u><</u>聽count聽<u><</u></font><font face="Times New Roman, Times, Serif" size="3"> 11)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">and the loop termination condition is</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count聽></font><font face="Times New Roman, Times, Serif" size="3"> 10</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">The following sequence of implications leads us to the loop postcondition:</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> = 1 + 2 + + </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3">-1) AND (2 </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3"><u><</u>聽count聽<u><</u></font><font face="Times New Roman, Times, Serif" size="3">11) AND (</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count聽></font><font face="Times New Roman, Times, Serif" size="3"> 10)</font><font face="Symbol" size="3">(r)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> = 1 + 2 + + </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3">-1) AND (</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> = 11)</font><font face="Symbol" size="3">(r)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> = 1 + 2 + + 10) AND (</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> = 11)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Times New Roman, Times, Serif" size="3">Placing a loop invariant into a While loop (or a For loop) is complicated by the fact that its loop test is at the top, not the bottom. To locate the loop invariant just before the loop test, we need two copies of the invariant, one before the loop starts and one at the end of an iteration:</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table border="0" cellspacing="0" cellpadding="0"><tr><td rowspan="5"></td> <td colspan="3" height="12"></td> <td rowspan="5"></td></tr><tr><td colspan="3"></td></tr><tr><td></td> <td><font face="Courier New, Courier, Mono New, Courier, Mono" size="2">//聽Invariant:聽<br />while聽(聽聽)<br />{<br />聽聽聽聽.<br />聽聽聽聽.<br />聽聽聽聽.<br /><br />聽聽聽聽//聽Invariant:聽<br />}</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td></tr></table><p><font size="0"></font></p>聽 </td> </tr> <tr> <td align="left" width="30%" style="background: #EEF3E2"><a style="color: blue; font-size: 120%; font-weight: bold; text-decoration: none; font-family: verdana;" href="page_475.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_476</strong></td> <td align="right" width="30%" style="background: #EEF3E2"><a style="color: blue; font-size: 120%; font-weight: bold; text-decoration: none; font-family: verdana;" href="page_477.html">next page ></a></td> </tr> </table> </body> </html>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -