Proof of Program Correctness - Loop Invariants

Question

I've been reading a book on using loop invariants and induction to prove program correctness. Then I came across the following program which got me thinking...

Specification for Cube_Root(n)

Pre-Condition: $n$ is a natural number. Post-Condition: Cube_Root returns a natural number $i$ that is the cube root of $n$ or it returns $-1$ if no such root exists

Cube_Root(n)
  i = 0
  while i < n
    if i * i * i = n
      return(i)
    else
      i = i + 1

  return(-1)

In the book, the proof proceeds by finding a loop invariant. So for example let us define the following as our loop invariant:

Loop Invariant $P(i)$: $i$ is either the natural number cube root of $n$ or $i \geq n$. The proof is then supposed to proceed by induction on $i$. So we need to prove that $P(0)$ is true, assume that $P(i)$ is true for some $i$ and then establish that if $P(i)$ is true then $P(i+1)$ is true.

$P(0)$ is trivial to prove true: if $n = 0$ then $i$ is a natural number and the the cube root of $n$ otherwise $n > 0$ (since $n$ is a natural number) and hence $i < n$.

However, the problem arises when you try to infer $P(i+1)$ from $P(i)$. it doesn't look like you can because if $i$ is not the cube root of $n$, it doesn't tell you anything about whether $i+1$ is or is not the cube root of $n$.

So my question(s) are:

1. Has it been proven that for any program there exists a loop invariant on which you can use induction to prove the program is correct?

2. The loop invariant chosen for Cube_Root is obviously true after the loop terminates which proves that the post-condition of the program is satisfied. Hence, that proves partial correctness of the program. However, we did not need to use induction to prove that. Is that an acceptable proof? If not, how do we use induction to prove Cube_Root correct?

Answer 1

Generalities

Regarding your first question, the correctness of every loop (without fancy control flow!) can always be proven using a loop invariant which states all the possible values of all variables. In your case (or rather in the modification below), this loop invariant would be $$ (n,i,r) \in \{(0,0,-1),(0,0,0),(1,0,-1),(1,1,-1),(1,1,1),(2,0,-1),(2,1,-1),(2,2,-1),(2,3,-1), \ldots \}. $$ Of course, this invariant isn't particularly helpful, though it can certainly be used to prove the correctness of the loop. A more delicate issue is whether we can actually express the invariant in any formal sense - when the loop always terminates as in this case, the set of possible values of the variables is certainly computable.

Regarding your second question, when you're using a loop invariant you always reason by induction - that's how you know that the loop invariant is actually maintained. Consider the following problem:

x, y = 0, 1
for i in range(n):
    x, y = y, x + y
return x

I claim that this program computes the $n$th Fibonacci number $F_n$. Here is a "loop invariant" that can be used to prove it: if $i = n$ then $x = F_n$. Of course, this is not really a loop invariant since you can't prove that it's maintained by the loop; an actual loop invariant is $(x,y) = (F_i,F_{i+1})$.

Your suggested loop invariant is like the first example above - it's simply not a loop invariant, and in particular it's not clear how you'd prove that if the loop terminates then it holds. It might seem "trivial", but this argument doesn't constitute a formal proof. In contrast, if you use an actual loop invariant, then you can use induction to prove that the loop invariant is maintained throughout the loop, and in particular is satisfied if the loop terminates. That's more formal, and can be turned into an actual formal proof (in the sense of program verification or axiomatic logic).

Whether your type of proof is acceptable or not depends on the venue. If this is a question in a course in which you're supposed to learn how to write this kind of formal proofs, then your answer isn't acceptable. In an algorithms class, it might be acceptable since the proof is "obvious". Ask your professor if in doubt.

Specifics

We now turn to the problem at hand.

The idea of a loop invariant is a condition which is true throughout the loop. As you mention, the condition that you describe is only true after the loop terminates (in the return statement). Ergo, it's not the correct condition. First, let's modify the program in the following way: instead of returning $i$, let's have a variable $r$ initialized with $-1$; when $i^3 = n$, assign $r = i$ and break out of the loop. Throughout the loop one of the following is always true, assuming $n > 1$ (for $n = 0,1$ the program fails; the condition in the main loop needs to be $i \leq n$ instead of $i < n$):

1. $i^3 < n$ and $r = -1$.
2. $i^3 = n$. In this case, $r = -1$ if the loop hasn't terminated, and $r = i$ otherwise.
3. $\sqrt[3]{n} \notin \mathbb{Z}$ and $i^3 > n$ and $r = -1$.

The second condition isn't quite of the usual form, and that is because usually break statements are not allowed. You can correct this by modifying the code as follows (this code also corrects the bug mentioned above):

r = -1
i = 0
while i <= n and r == -1:
    if i*i*i == n:
        r = i
        continue
    else:
        i = i + 1
return r

Now the loop invariant becomes:

1. $i^3 < n$ and $r = -1$.
2. $i^3 = n$ and $r \in \{-1,i\}$.
3. $\sqrt[3]{n} \notin \mathbb{Z}$ and $i^3>n$ and $r = -1$.

Now the loop termination condition makes it clear that if $i \leq n$ then necessarily $r \neq -1$, and so by the loop invariant, $r = i$.