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

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

  public static int maximumElement2(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 void overwrite(int[] a, int p, int n, int x)
  {
    for (int i=p; i<p+n; i++)
      a[i] = x;
  }
  
  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 i = 0; i < n; i++)
      b[p+i] = x;
    for (int i = p; i < m; i++)
      b[n+i] = a[i];
    return b;
  }

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

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

  public static void subtract2(int[] a, int[] b) throws Truncated
  {
    int n = a.length;
    for (int i = 0; i < n; i++)
    {
      if (a[i] < b[i]) throw new Truncated(i);
      a[i] = a[i]-b[i];
    }
  }
}