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:
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?
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?