📄 page_307.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd"> <html> <head> <title>page_307</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_306.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_307</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_308.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 307</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="Times New Roman, Times, Serif" size="3">where the symbol </font><font face="Symbol" size="3">(r)</font><font face="Times New Roman, Times, Serif" size="3"> is the <i>logical implication</i> operator and is pronounced <i>implies.</i> In other words, we want to ensure that <i>if</i> the invariant is true and the While condition is false, <i>then</i> the loop 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">The loop invariant usually consists of other conditions as well as those related to the While condition. For example, it typically includes the ranges of all the variables used in the loop and the status of any files.</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 create the invariant, we begin with the loop postconditionour answer to the last question on the loop design checklist (<i>What is the state of the program on exiting the loop?)</i>because it forces us to determine the final condition of the variables and files. Then we work backward, answering the other questions on the checklist.</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">Let's write the invariant for the outer loop in the Invoice program. We begin with the part of the invariant associated with </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">totalAmount.</font><font face="Times New Roman, Times, Serif" size="3"> We know that on loop exit, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">totalAmount</font><font face="Times New Roman, Times, Serif" size="3"> contains the sum of all the individual item amounts. Then we look at how the process is initialized and updated. Here's the related invariant condition:</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"><img src="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" border="0" width="0" height="1" alt="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" /></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">totalAmount</font><font face="Times New Roman, Times, Serif" size="3"> >= 0 AND<br />At the start of each iteration, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">totalAmount</font><font face="Times New Roman, Times, Serif" size="3"> equals the total of all the values of </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">amount</font><font face="Times New Roman, Times, Serif" size="3"> that have been computed.</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">In the same way, we look at the termination condition, initialization, and update of </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">totalUnits</font><font face="Times New Roman, Times, Serif" size="3"> to determine the portion of the invariant that relates to it:</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"><img src="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" border="0" width="0" height="1" alt="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" /></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">totalUnits</font><font face="Times New Roman, Times, Serif" size="3"> >= 0 AND<br />At the start of each iteration, </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">totalUnits</font><font face="Times New Roman, Times, Serif" size="3"> equals the sum of all the values of </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">quantity</font><font face="Times New Roman, Times, Serif" size="3"> that have been input so far.</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">Here are the invariant conditions for the other variables and the input file:</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">price</font><font face="Times New Roman, Times, Serif" size="3"> either is undefined or contains a floating point value AND<br /></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">price</font><font face="Times New Roman, Times, Serif" size="3"> contains the item price input in the most recently completed 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"></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">amount</font><font face="Times New Roman, Times, Serif" size="3"> either is undefined or contains a floating point value AND<br /></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">amount</font><font face="Times New Roman, Times, Serif" size="3"> contains the product </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">quantity聽*聽price</font><font face="Times New Roman, Times, Serif" size="3"> calculated in the most recently completed 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"></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">quantity</font><font face="Times New Roman, Times, Serif" size="3"> contains the most recently input quantity ordered of an item.</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">counter</font><font face="Times New Roman, Times, Serif" size="3"> either is undefined or contains the value 31.</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">inputChar</font><font face="Times New Roman, Times, Serif" size="3"> either is undefined or contains the last character of the item description input in the previous 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"></font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">blank</font><font face="Times New Roman, Times, Serif" size="3"> either is undefined or contains the character between the quantity and the item description input in the previous 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"> The reading marker in </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">inFile</font><font face="Times New Roman, Times, Serif" size="3"> is positioned just after the most recent quantity input.</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">In addition to the status of variables and files, most programs contain some general invariant conditions. For example:</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_306.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_307</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_308.html">next page ></a></td> </tr> </table> </body> </html>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -