The above proof technique
enables us to establish the
"partial correctness" of a program
{Pre} Program {Post}
If pre condition holds, and the program
properly exits, then the post condition
must also hold.
However, if the program does not
terminate, we cannot guarantee it.
A "total correctness proof" must
also establish that the program
actually terminates.