Incremental Java
Loop Postcondition

Condition and Exiting

For every loop construct we've seen (while, do while, and for), you exit the loop when the loop condition evaluates to false.

What condition must therefore be true, immediately after we exit the loop? This condition is called the postcondition.

Since the loop condition is false, then its negation must be true.

Thus, the loop condition and the postcondition must be negations of each other.

Here's an example: 

int i ;
for ( i = 0 ; i < num ; i++ )
{
  // CODE
}
// Postcondition: i >= num
Recall the negation of i < num is i >= num.

Why Postconditions?

Sometimes it's hard to write a loop condition, though it's easier to write a loop postcondition. For example, suppose you are asking a person to enter a number. You want to guarantee the number is between 1 and 5. If there is a mistake, i.e., they pick a number too big or too small, then you want the person to re-enter the number.

The postcondition is choice >= 1 && choice <= 5, which means the choice must be between 1 and 5.

This must make the condition the negation of this, which we can write as: !( choice >= 1 && choice <= 5 ). Here's the code for this: 

System.out.print( "Enter a number: " ) ;
int val = FakeIO.readNum() ;
while ( !( choice >= 1 && choice <= 5 )
{
   System.out.println( "Error: number must be between 1 and 5" ) ;
   System.out.print( "Enter a number: " ) ;
   int val = FakeIO.readNum() ;
}
// Postcondition: choice >= 1 && choice <= 5,
We assumed a class called FakeIO (as you might guess, it doesn't exist), which has a static method called readNum() which allows us to read what the user types in.

Unfortunately, Java doesn't have easy-to-use input methods. However, System.out.println() is easy-to-use for printing output. It's puzzling why they didn't write something as simple for input.