Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `numbers.length >= 0` (established by the implementor of the array type) imply it.
Inductively assume that prior iterations of the loop preserved the invariant and didn't perform any invalid indexing operations. Now, every time the loop's condition is evaluated, there are two possibilities: either `0 <= index == numbers.length` or `0 <= index < numbers.length`. In the former case, the loop terminates and no further indexing operations are used, establishing the claim. In the latter case, `numbers[index]` is a valid indexing operation, and the subsequent `index++` operation does not destroy the invariant, because, given the precondition `0 <= index < numbers.length`, the operation `index++` establishes the postcondition `0 < index <= numbers.length`, which implies the invariant.
---
Note, however, that in this case it would have been more efficient to use an iterator, because the iterator's implementation already packages this proof in a reusable way, so that you don't need to reprove it every time you write a loop similar to this.