/*@ requires 0 <= m < n <= a.length;
    @ behavior mn_reverse:
    @   ensures \forall integer i; m <= i < n ==> \old(a)[i]==a[n+m-i-1];
    @*/
    public static int[] Reverse(int a[], int m, int n)
    {
        int[] A = new int[a.length];
        /*@ loop_invariant
        @ (\forall integer j; (m <= j < i) ==> (A[j] == a[j]));
        @*/
        for (int i = 0; i < a.length; i++)
        {
                A[i] = a[i];
        }

        int k = (m+n) / 2;
        //@ ghost int[] a_0 = a;
        /*@ loop_invariant m <= i <= k &&
        @ (\forall integer j; (m <= j < i) ==> (a[n+m-j-1] == a_0[j])) &&
        @ (\forall integer l; (n+m-i-1 <= l < n) ==> (a[l] == a_0[n+m-l-1]));
        @ loop_variant n-i;
        @*/
        for (int i = m; i < k; i++)
        {
                int temp = a[n+m-i-1];
            a[n+m-i-1] = a[i];
            a[i] = temp;
        }
        return a;
    }