Program Logic and Indefinite Loops - Building Java Programs: A Back to Basics Approach - page 340

the uncertainty of user input, this particular assertion may sometimes be true and some-
times false. But something later in the program may depend on the assertion being true.
For example, if you are going to take the square root of that number, you must be sure
the number is nonnegative. Otherwise, you might end up with a bad result.
Using a loop, you can guarantee that the number you get is nonnegative:

System.out.print("Please give me a nonnegative number——> ");
double number = console.nextDouble();
while (number < 0.0) {
System.out.print("That is a negative number. Try again——> ");
number = console.nextDouble();

}
// is number nonnegative?

You know that number will be nonnegative after the loop; otherwise, the program
would not exit the while loop. As long as a user gives negative values, your program
stays in the while loop and continues to prompt for input.
This doesn't mean that number should be nonnegative after the loop. It means that
number will be nonnegative. By working through the logic of the program, you can
see that this is a certainty, an assertion of which you are sure. You could even prove it
if need be. Such an assertion is called a provable assertion .

Provable Assertion
An assertion that can be proven to be true at a particular point in program
execution.

Provable assertions help to identify unnecessary bits of code. Consider the follow-
ing statements:

int x = 0;
if (x == 0) {
System.out.println("This is what I expect.");
} else {
System.out.println("How can that be?");

}

The if/else construct is not necessary. You know what the assignment statement
does, so you know that it sets x to 0 . Testing whether x is 0 is as unnecessary as saying,
“Before I proceed, I'm going to check that 2 2 equals 4.” Because the if part of

this if/else statement is always executed, you can prove that the following lines of
code always do the same thing as the preceding lines:

int x = 0;
System.out.println("This is what I expect.");