|
|
|
|
|
|
|
is undefined. (For example, if count equals zero, the postcondition surely isn't satisfiedthe program crashes!) |
|
|
|
|
|
|
|
|
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: |
|
|
|
|
|
|
|
|
void Get2Ints( int& int1,
int& int2 )
// Postcondition:
// User has been prompted to enter two integers
// && int1 == first input value
// && int2 == second input value
{
cout << Please enter two integers: ;
cin >> int1 >> int2;
} |
|
|
|
|
|
|
|
|
In assertions written as C++ comments, we use either && or AND to denote the logical AND operator; either || or OR to denote a logical OR; either ! or NOT to denote a logical NOT; and == to denote equals. (Notice that we do not use = to denote equals. Even when we write program comments, we want to keep C++'s == operator distinct from the assignment operator.) |
|
|
|
|
|
|
|
|
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 @entry to the end of the variable name. Below is an example of the use of this notation. The Swap function exchanges, or swaps, the values of its two parameters. |
|
|
|
|
|
|
|
|
void Swap( int& firstInt,
int& secondInt )
// Precondition:
// firstInt and secondInt are assigned
// Postcondition:
// firstInt == secondInt@entry
// && secondInt == firstInt@entry
{
int temporaryInt;
|
|
|
|
|
|