@requires a[i] = 1 && a[j] = 2 && i = 10 && j = 20
@ensures  a[10] = 2 && a[20] = 1 

@program 

  @var i, j, temp : int
  @var a : int[]

   temp = a[i];
   a[i] = a[j];
   a[j] = temp;

@end
--