@requires n > 1 && a[0] =< pivot && a[n-1] >= pivot

@ensures all(k, 0:high-1, a[k] =< pivot) &&
         all(k, high+1:n-1, a[k] > pivot)

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

    low = 0;
    high = n-1;
    
    @invariant 0 =< low && low =< high && high =< n-1 &&
               all(k, 0:low-2, a[k] =< pivot) &&
               all(k, high+2:n-1, a[k] > pivot) &&
               a[low-1] =< pivot && a[high+1] > pivot
    while (low < high) {  

       // the code below ensures that both inner loops
       // will not break without changing low/high

        @invariant 0 =< low && low =< high && high =< n-1 &&
               all(k, 0:low-2, a[k] =< pivot) &&
               all(k, high+2:n-1, a[k] > pivot) &&
               a[low-1] =< pivot && a[high+1] > pivot
	while (low < high) {
            if (a[low] > pivot)
            	  break;
            low = low + 1;
        }

        @invariant 0 =< low && low =< high && high =< n-1 &&
               all(k, 0:low-2, a[k] =< pivot) &&
               all(k, high+2:n-1, a[k] > pivot) &&
               a[low-1] =< pivot && a[high+1] > pivot
	while (low < high) {
            if (a[high] =< pivot)
            	  break;
            high = high - 1;
       }
    //  if (a[low] > pivot && a[high] =< pivot) {
       temp = a[low];
       a[low] = a[high];
       a[high] = temp;
   //  }   
}

@end
--