proof of correctness by loop invariant (induction)

I wrote my own trivial little function (php for convenience) and was hoping someone could help structure a proof by induction for it, just so I can get a very basic hang of it.

function add_numbers($max) {
  //assume max >= 2
  $index=1;
  $array=array(0);
  while ($index != $max) {
     //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
     $array[$index] = $array[$index-1]+1;
     $index += 1;
  }
}

The result being that the value at each index is the same as the index itself, though only because a[0] was initialized to 0.

I believe the goal is (or should be) to prove that the invariant (which may itself be suspect, but hopefully gets the point across) holds for k+1.

Thanks

edit: examples: http://homepages.ius.edu/rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm

Solution

Something like this, maybe, although this is a little pedantic.

Invariant: when index = n, for n >= 1 (at the top of the loop where it checks the condition), array[i] = i for 0 <= i < n.

Proof: The proof is by induction. In the base case n = 1, the loop is checking the condition for the first time, the body has not executed, and we have an outside guarantee that array[0] = 0, from earlier in the code. Assume the invariant holds for all n up to k. For k + 1, we assign array[k] = array[k-1] + 1. From the induction hypothesis, array[k-1] = k-1, so the value assigned array[k] is (k-1)+1 = k. Thus the invariant holds for the next, and by induction every, value of n (at the top of the loop).

EDIT:

function add_numbers($max) {
  //assume max >= 2
  $index=1;
  $array=array(63);
  while ($index != $max) {
     //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
     $array[$index] = $array[$index-1]+1;
     $index += 1;
  }
}

Invariant: when index = n, for n >= 1 (at the top of the loop where it checks the condition), array[i] = i + 63 for 0 <= i < n.

Proof: The proof is by induction. In the base case n = 1, the loop is checking the condition for the first time, the body has not executed, and we have an outside guarantee that array[0] = 63, from earlier in the code. Assume the invariant holds for all n up to k. For k + 1, we assign array[k] = array[k-1] + 1. From the induction hypothesis, array[k-1] = (k-1) + 63 = k + 62, so the value assigned array[k] is (k+62)+1 = k+63. Thus the invariant holds for the next, and by induction every, value of n (at the top of the loop).