📄 page_306.html

📁 Programming and Problem Solving with C++
💻 HTML
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">	<html>		<head>			<title>page_306</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_305.html">&lt;&nbsp;previous page</a></td>				<td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_306</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_307.html">next page&nbsp;&gt;</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 306</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">precondition and postcondition for a loop, we must determine those characteristics that do not vary from one iteration to the next. The collection of all these characteristics is called the loop invariant, an assertion that must always be true for the loop to execute correctly.</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" width="100%"><tr><td rowspan="5"><img src="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" border="0" width="96" height="1" alt="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" /></td>  <td colspan="3" height="12"></td>  <td rowspan="5"><img src="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" border="0" width="96" height="1" alt="3e26ecb1b6ac508ae10a0e39d2fb98b2.gif" /></td></tr><tr><td colspan="3" height="2"><table cellpadding="0" cellspacing="0" border="0"><tr><td></td></tr></table></td></tr><tr><td></td>  <td><font face="Times New Roman, Times, Serif" size="2">Loop Invariant An assertion about the characteristics of a loop that must always be true for a loop to execute properly. The invariant is true on loop entry, at the start of each loop iteration, and on exit from the loop. It is not necessarily true at each point in the body of the loop.</font></td><td></td></tr><tr><td colspan="3" height="2"><table cellpadding="0" cellspacing="0" border="0"><tr><td></td></tr></table></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 first, you might think that the invariant is just the While condition that controls the loop. But an invariant must be TRUE when the loop exits; the While condition is FALSE when the loop exits. Here are some examples:</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table><table cellpadding="0" cellspacing="0" border="0" width="100%"><tr><td height="12"></td></tr><tr><td><table cellspacing="0" width="614" cellpadding="7"><tr><td valign="top"><table border="0" cellspacing="0" cellpadding="0" width="100%"><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 align="center"><font face="Times New Roman, Times, Serif" size="3"><i>While-Loop Condition</i></font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td><td valign="top"><table border="0" cellspacing="0" cellpadding="0" width="100%"><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 align="center"><font face="Times New Roman, Times, Serif" size="3"><i>Related Invariant Condition</i></font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td></tr><tr><td valign="top"><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="Courier New, Courier, Mono New, Courier, Mono" size="3">loopControlVariable</font><font face="Times New Roman, Times, Serif" size="3"> &lt;366<br />(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">loopControlVariable</font><font face="Times New Roman, Times, Serif" size="3"> is initialized to 1 before the loop.)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td><td valign="top"><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&lt;=</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">loopControlVariable</font><font face="Times New Roman, Times, Serif" size="3">&lt;=366</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td></tr><tr><td valign="top"><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="Courier New, Courier, Mono New, Courier, Mono" size="3">oddCount</font><font face="Times New Roman, Times, Serif" size="3"> &lt;10<br />(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">oddCount</font><font face="Times New Roman, Times, Serif" size="3"> is initialized to 0 before the loop.)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td><td valign="top"><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="Courier New, Courier, Mono New, Courier, Mono" size="3">oddCount</font><font face="Times New Roman, Times, Serif" size="3"> equals the number of odd numbers input AND<br />0&lt;=</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">oddCount</font><font face="Times New Roman, Times, Serif" size="3">&lt;=10</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td></tr><tr><td valign="top"><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="Courier New, Courier, Mono New, Courier, Mono" size="3">inputVal</font><font face="Times New Roman, Times, Serif" size="3">&gt;=0<br />(</font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">inputVal</font><font face="Times New Roman, Times, Serif" size="3"> is initialized before the loop.)</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td><td valign="top"><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">Only nonnegative data values are processed AND </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">inputVal</font><font face="Times New Roman, Times, Serif" size="3">&lt;0 when the loop exits</font></td><td></td></tr><tr><td colspan="3"></td></tr><tr><td colspan="3" height="1"></td></tr></table></td></tr></table></td></tr></table><br /><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">You can see that an invariant condition is related to each While condition but that they are not identical. The loop invariant and the While condition must be true for the loop to execute; the loop invariant and the termination condition (the negation of the While condition) must be true after the loop exits. Let's state this relationship more precisely using logic symbols. Suppose we have a loop with While condition <i>C:</i></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">while聽(<i>C)<br /></i>聽聽Statement</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">Suppose further that the loop invariant is <i>I</i> and that <i>P</i> is the loop postcondition (the assertion that is true immediately after loop exit). Then the following 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="Times New Roman, Times, Serif" size="3">(<i>I</i> AND (NOT <i>C))</i> </font><font face="Symbol" size="3">(r)</font><font face="Times New Roman, Times, Serif" size="3"> <i>P</i></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_305.html">&lt;&nbsp;previous page</a></td>				<td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_306</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_307.html">next page&nbsp;&gt;</a></td>			</tr>		</table>		</body>	</html>
⌨️ 快捷键说明

复制代码 Ctrl + C
搜索代码 Ctrl + F
全屏模式 F11
切换主题 Ctrl + Shift + D
显示快捷键 ?
增大字号 Ctrl + =
减小字号 Ctrl + -