package Arrays1;

public class Arrays1
{
  /*@ public normal_behavior
    @ requires
    @   a != null && a.length >= 0 &&
    @   0 <= p && p <= a.length;
    @ assignable
    @   \nothing;
    @ ensures
    @   (\forall int i; 0 <= i && i < p;
    @       a[i] == \result[i]
    @   ) &&
    @   (\forall int i; p <= i && i < a.length;
    @       a[i] == \result[i+1]
    @   ) &&
    @   x == \result[p];
    @*/
  public static int[] insert(int[] a, int x, int p)
  {
    int[] b = new int[a.length+1];
    int n = a.length;
    int i=0;
    /*@ loop_invariant
      @   a != null && a.length >= 0 && n == a.length &&
      @   b != null && b.length >= 0 && b.length == n + 1 &&
      @   0 <= p && p <= n &&
      @   0 <= i && i <= n+1 &&
      @   (\forall int j; j < i && 0 <= j && j < p;
      @       a[j] == b[j]
      @   ) &&
      @   (\forall int j; j < i-1 && p <= j && j < n;
      @       a[j] == b[j+1]
      @   ) &&
      @   ( p >= i || x == b[p] );
      @ decreases
      @   n + 1 - i;
      @ assignable
      @   i,b,b[*];
      @*/
    while( i < n+1 )
    {
      if (i < p)
        b[i] = a[i];
      else if (i == p)
        b[i] = x;
      else
        b[i] = a[i-1];
      i = i+1;
    }
    return b;
  }
}