public class Exercise5
{
  public static void main(String[] args)
  {
    // test calls here
  }

 public static int maximumIndex(int[] a)
  {
    int m = 0;
    int n = a.length;
    for (int i = 1; i < n; i++)
    {
      if (a[i] > a[m]) m = i;
    }
    return m;
  }

  public static int maximumElement1(int[] a)
  {
    int p = maximumIndex(a);
    return a[p];
  }

  public static int maximumElement2(int[] a)
  {
    int m = 0;
    int n = a.length;
    for (int i = 1; i < n; i++)
    {
      if (a[i] > m) m = a[i];
    }
    return m;
  }

  public static int[] insert(int[] a, int p, int n, int x)
  {
    int m = a.length;
    int[] b = new int[m+n];
    for (int i = 0; i < p; i++)
      b[i] = a[i];
    for (int j = p; j < p+n; j++)
      b[j] = x;
    for (int k = p+n; k < m+n; k++)
      b[k] = a[k];
    return b;
  }

  public static int replace(char[] a, char x, char y)
  {
    int n = a.length;
    int result = -1;
    for (int i = 0; i <= n; i++)
    {
      if (a[i] == x) 
      {
        a[i] = y;
        if (result == -1) result = i;
      }
    }
    return result;
  }

  public static boolean add1(int[] a, int[] b)
  {
    int n = a.length;
    boolean overflow = false;
    for (int i = 0; i < n; i++)
    {
      if (a[i] > Integer.MAX_VALUE-b[i]) 
        overflow = true;
      else
        a[i] += b[i];
    }
    return overflow;
  }

  public static void add2(int[] a, int[] b) throws Overflow
  {
    int n = a.length;
    for (int i = 0; i < n; i++)
    {
      if (a[i] > Integer.MAX_VALUE-b[i]) 
        throw new Overflow(i);
      else
        a[i] += b[i];
    }
  }

  public static class Overflow extends Exception 
  { 
    public final int pos;
    /*@ public normal_behavior
      @ requires true;
      @ assignable this.pos;
      @ ensures this.pos == pos;
      @*/
    public Overflow(int pos) { this.pos = pos; }
  }
}