public class Array
{
  // copy content of a starting with index i into b
  //@ requires a != null && b != null;
  //@ requires 0 <= i && i+b.length <= a.length;
  /*@ ensures (\forall int j; 0 <= j && j < b.length; 
    @           b[j] == a[i+j]); @*/
  public static void copy(int[] a, int i, int[] b)
  {
    int n = b.length;
    for (int j = 0; j < n; j++)
      b[j] = a[j+i];
  }

  // return subarray a[i..i+n-1]
  //@ requires a != null;
  //@ requires 0 <= i && 0<= n && i+n <= a.length;
  //@ ensures \result != null && \result.length == n;
  /*@ ensures (\forall int j; 0 <= j && j < \result.length; 
    @             \result[j] == a[i+j]); @*/
  public static int[] subarray(int[] a, int i, int n)
  {
    int[] b = new int[n];
    copy(a, i, b);
    return b;
  }

  // return subarray of a starting at i
  //@ requires a != null;
  //@ requires 0 <= i && i <= a.length;
  //@ ensures \result != null && \result.length == a.length-i;
  /*@ ensures (\forall int j; 0 <= j && j < \result.length; 
    @            \result[j] == a[i+j]); @*/
  public static int[] subarray(int[] a, int i)
  {
    return subarray(a, i, a.length-i);
  }
}