📄 page_310.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd"> <html> <head> <title>page_310</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_309.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_310</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_311.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 310</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">聽聽聽聽while聽(number聽<=聽10)<br />聽聽聽聽{<br />聽聽聽聽聽聽聽聽sum聽=聽sum聽+聽number;<br />聽聽聽聽聽聽聽聽number++;<br />聽聽聽聽}<br />}</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">To verify this program, we begin by determining the loop postcondition. When the loop finishes executing, here's what should be true:</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">sum</font><font face="Times New Roman, Times, Serif" size="3"> contains the sum of the integers from 0 through 10 AND<br /></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> equals 11 AND<br />The number of loop iterations executed equals 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">Now we have to do the following:</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">1. Define the loop invariant.</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">2. Show that the invariant is true before loop entry.</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">3. Show that the invariant is true at the start of each 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="Times New Roman, Times, Serif" size="3">4. Show that at loop exit the invariant is still true, the termination condition is true, and the AND of these two conditions implies that the postcondition is true.</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">This is the loop invariant:</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">sum</font><font face="Times New Roman, Times, Serif" size="3"> contains the sum of the integers from 0 through </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1聽AND<br />1聽<=聽number聽<=聽11聽AND<br /></font><font face="Times New Roman, Times, Serif" size="3">The number of loop iterations executed equals </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1.</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">At loop entry, the following conditions have been established: </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> is equal to 0, and </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> is equal to 1. Comparing these conditions to the invariant, we see that </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> is equal to </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1;聽number</font><font face="Times New Roman, Times, Serif" size="3"> is in the range 1 through 11; and the number of iterations executed is 0, which equals </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1</font><font face="Times New Roman, Times, Serif" size="3">.</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">Next, we walk through the loop body. The first statement adds the value of </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽to聽sum,</font><font face="Times New Roman, Times, Serif" size="3"> so </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> now contains the sum of the integers from 0 through </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number.</font><font face="Times New Roman, Times, Serif" size="3"> The next statement increments </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number,</font><font face="Times New Roman, Times, Serif" size="3"> which means that </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">sum</font><font face="Times New Roman, Times, Serif" size="3"> now contains the sum of the integers from 0 through </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1.</font><font face="Times New Roman, Times, Serif" size="3"> At the end of this iteration, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number聽-聽1</font><font face="Times New Roman, Times, Serif" size="3"> also equals the number of iterations. Because </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> cannot be greater than 10 at the start of an iteration, we also know that </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> cannot be greater than 11 at this point. So the invariant is true for the start of the next 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="Times New Roman, Times, Serif" size="3">We can tell that the loop terminates correctly from the fact that </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> is initially less than 10 and is incremented in each loop iteration. So </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">number</font><font face="Times New Roman, Times, Serif" size="3"> eventually becomes greater than 10, and the loop will terminate.</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">Finally, let's form the logical AND of the loop invariant and the termination condition:</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_309.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_310</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_311.html">next page ></a></td> </tr> </table> </body> </html>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -