package exercises;

public class Exercise5a
{
  public static int[] olda; // models \old(a) in loop invariant

  /*@ requires olda != a && olda != null && olda.length == a.length &&
    @          (\forall int j; 0 <= j && j < a.length; olda[j] == a[j]);
    @ requires ...
    @ assignable ...
    @ ensures ...
    @*/
  public static void invert(int[] a)
  {
    int i = 0;
    int n = a.length;
    /*@ loop_invariant 
      @  olda != a && olda != null && a.length == olda.length &&
      @  ...
      @ assignable ...
      @ decreases ...
      @*/
    while (2*i+1 < n) 
    {
      int b = a[i];
      a[i] = a[n-i-1];
      a[n-i-1] = b;
      i = i+1;
    }
  }
}