Proof of Program Correctness - Loop Invariants
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 &gt; 1$ (for $n = 0,1$ the program fails; the condition in the main loop needs to be $i \leq n$ instead of $i &lt; n$):


$i^3 &lt; n$ and $r = -1$.
$i^3 = n$. In this case, $r = -1$ if the loop hasn't terminated, and $r = i$ otherwise.
$\sqrt[3]{n} \notin \mathbb{Z}$ and $i^3 &gt; 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 &lt;= n and r == -1:
    if i*i*i == n:
        r = i
        continue
    else:
        i = i + 1
return r


Now the loop invariant becomes:


$i^3 &lt; n$ and $r = -1$.
$i^3 = n$ and $r \in \{-1,i\}$.
$\sqrt[3]{n} \notin \mathbb{Z}$ and $i^3&gt;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$.