First Steps in Theorem Proving using KeY

Now something very technical! I'll try to keep it simple; as simple as possible, but not any simpler.

Following is a .key file that has Java code in between \<{ and }\>. The code looks for the maximum element in the array. The first order logical formula (after the block of code) says that when the code has been executed, the variable max will hold a value greater than or equal to every element of the array.

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   for (int i=0; i<a.length; i++) {
    if (a[i] > max) max = a[i];
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

This format is internal to the KeY tool. But the ideas will be similar to any theorem prover for imperative programming languages, like Java.

At the moment, I am stuck up because there is no upper limit on the size of the array, which tells me that the only way to prove the formula is to use induction. Now, the only sequence that can be made a basis for induction is the size of the array. I'm trying to figure out how to state this in KeY.