@requires n >= 1 && all(k, 0:n-1, a[k] = olda[k])

@ensures all(k, 0:n-1, a[k] = olda[n-k-1])

// all(k, 0:high-1, a[k] = olda[n-k-1]) &&
// all(k, high+1:n-1, a[k] = olda[n-k-1])

@program 

  @var low, high, n, temp : int
  @var a, olda : int[]

  low = 0;
  high = n-1;

  @invariant 
    0 =< low && high < n && low =< n &&
    (high + low = n-1) &&
     all(k, 0:low-2, a[k] = olda[n-k-1]) && 
     all(k, high+2:n-1, a[k] = olda[n-k-1]) && 
    all(k, low:high, a[k] = olda[k]) &&
     a[low-1] = olda[n-low] &&
     a[high+1] = olda[n-high-2] 

  while (low < high) {
     temp = a[low];
     a[low] = a[high];
     a[high] = temp;
     low = low + 1;
     high = high - 1;
  }

@end
--