proc pivot(l0: int, r0:int) returns (middle: int)
var l: int, r: int;
begin
  l = l0; r = r0;
  while l < r do
    if brandom then
      l = l+1;
    else
      r = r-1;
    endif;
  done; 
  middle = l;
end

proc quicksort(l: int, r: int) returns ()
var mid: int, tmp: int;
begin
  if r > l
  then
    mid = pivot(l, r);
    tmp = mid-1;
    () = quicksort(l, tmp);
    tmp = mid+1;
    () = quicksort(tmp, r);
  endif;
end

var l0: int, n: int, middle: int;
begin
  l0 = 1;
  assume n >= l0;
  () = quicksort(l0, n);
end
