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

Thus, you can conclude that after the loop is done executing, the test can no longer
be true:
while (<test>) {
// test is always true here
...
}
// test is never true here
The test can't be true after the loop because if it had been true, the program would
have executed the body of the loop again.
These observations about the properties of if statements, if/else statements,
and while loops provide a good start for proving certain assertions about programs.
But often, proving assertions requires a deeper analysis of what the code actually
does. For example, suppose you have a variable x of type int and you execute the
following if statement:
if (x < 0) {
// x < 0 is always true here
x = -x;
}
// but what about x < 0 here?
You wouldn't normally be able to conclude anything about x being less than 0
after the if statement, but you can draw a conclusion if you think about the different
cases. If x was greater than or equal to 0 before the if statement, it will still be
greater than or equal to 0 after the if statement. And if x was less than 0 before the
if statement, it will be equal to -x after. When x is less than 0 , -x is greater than 0 .
Thus, in either case, you know that after the if statement executes, x will be greater
than or equal to 0 .
Programmers naturally apply this kind of reasoning when writing programs.
Program-verification researchers are trying to figure out how to do this kind of rea-
soning in a formal, verifiable way.
A Detailed Assertions Example
To explore assertions further, let's take a detailed look at a code fragment and a set of
assertions we might make about the fragment. Consider the following method:
public static void printCommonPrefix(int x, int y) {
int z = 0;
// Point A
while (x != y) {
// Point B
z++;