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

 public static int minimumPosition(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 minimumElement(int[] a)
  {
    int p = minimumPosition(a);
    return a[p];
  }

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

  public static int[] overwrite(int[] a, int p, int n, int x)
  {
    int n0 = a.length;
    if (p+n > n0) n0 = p+n;
    int[] b = new int[n0];
    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 < a.length; 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;
        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]) 
      {
      	a[i] = Integer.MAX_VALUE;
        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; }
  }

}