class Max {
  
  
  //@ ensures (\forall int j; 0 <=j && j < a.length; a[j] <= \result);
  static int max(int[] a) {
    int m_index = 0;
    for (int i = 1; i< a.length; i++) {
      if (a[i] > a[m_index]) {
        m_index = i;
      }
    }
    return a[m_index];
  }

}