📄 page_355.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd"> <html> <head> <title>page_355</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_354.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_355</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_356.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 355</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">is undefined. (For example, if </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">count</font><font face="Times New Roman, Times, Serif" size="3"> equals zero, the postcondition surely isn't satisfiedthe program crashes!)</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">Sometimes the caller doesn't need to satisfy any precondition before calling a function. In this case, the precondition can be written as the value TRUE or simply omitted. In the following example, no precondition is necessary:</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">void聽Get2Ints(聽int&聽int1,<br />聽聽聽聽聽聽聽聽聽聽聽聽聽聽聽int&聽int2聽)<br /><br />//聽Postcondition:<br />//聽聽聽聽聽User聽has聽been聽prompted聽to聽enter聽two聽integers<br />//聽聽&&聽int1聽==聽first聽input聽value<br />//聽聽&&聽int2聽==聽second聽input聽value<br /><br />{<br />聽聽聽聽cout聽<<聽Please聽enter聽two聽integers:聽;<br />聽聽聽聽cin聽>>聽int1聽>>聽int2;<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">In assertions written as C++ comments, we use either </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">&&</font><font face="Times New Roman, Times, Serif" size="3"> or </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">AND</font><font face="Times New Roman, Times, Serif" size="3"> to denote the logical AND operator; either </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">||</font><font face="Times New Roman, Times, Serif" size="3"> or </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">OR</font><font face="Times New Roman, Times, Serif" size="3"> to denote a logical OR; either </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">!</font><font face="Times New Roman, Times, Serif" size="3"> or </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">NOT</font><font face="Times New Roman, Times, Serif" size="3"> to denote a logical NOT; and </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">==</font><font face="Times New Roman, Times, Serif" size="3"> to denote equals. (Notice that we do <i>not</i> use </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">=</font><font face="Times New Roman, Times, Serif" size="3"> to denote equals. Even when we write program comments, we want to keep C++'s </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">==</font><font face="Times New Roman, Times, Serif" size="3"> operator distinct from the assignment operator.)</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">There is one final notation we use when we express assertions as program comments. Preconditions implicitly refer to values of variables at the moment the function is invoked. Postconditions implicitly refer to values at the moment the function returns. But sometimes you need to write a postcondition that refers to parameter values that existed at the moment the function was invoked. To signify at the time of entry to the function, we attach the symbols </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">@entry</font><font face="Times New Roman, Times, Serif" size="3"> to the end of the variable name. Below is an example of the use of this notation. The </font><font face="Courier New, Courier, Mono New, Courier, Mono" size="3">Swap</font><font face="Times New Roman, Times, Serif" size="3"> function exchanges, or swaps, the values of its two parameters.</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">void聽Swap(聽int&聽firstInt,<br />聽聽聽聽聽聽聽聽聽聽聽int&聽secondInt聽)<br /><br />//聽Precondition:<br />//聽聽聽聽聽firstInt聽and聽secondInt聽are聽assigned<br />//聽Postcondition:<br />//聽聽聽聽聽firstInt聽==聽secondInt@entry<br />//聽&&聽secondInt聽==聽firstInt@entry<br /><br />{<br />聽聽聽聽int聽temporaryInt;<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_354.html">< previous page</a></td> <td align="center" width="40%" style="background: #EEF3E2"><strong style="color: #2F4F4F; font-size: 120%;">page_355</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_356.html">next page ></a></td> </tr> </table> </body> </html>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -