quick_sort_range(first, last: INTEGER) is
	 -- sort elements first..last into increasing order
	 -- (quick sort algorithm)
      require range_not_empty: first <= last
      local
	 i,j: INTEGER
      do
	 debug ("Recursion")
	    print("Entering quick_sort_range(")
	    print(first); print(','); print(last); print(")%N")
	 end -- debug
	 from i := first + 1; j := last
	 invariant
	    left_lower: max_value_in(first, i-1) <= item(first)
	    right_higher: (j < last) 
	    implies (min_value_in(j+1, last) > item(first))
	 variant ends_converging:  j - i + 2
	 until i > j 
	 loop
	    if item(i) <= item(first) then
	       i := i + 1	-- advances i rightwards
	    elseif item(j) > item(first) then
	       j := j - 1	-- advances j leftwards
	    else		-- i & j have been found
	       swap(i,j)	-- swap item(i) and item(j)
	       i := i + 1	-- next i & j
	       j := j - 1
	    end -- if
	 end -- loop
	 swap(first, j)		-- places back the pivot
	 if first < j - 1 then quick_sort_range(first, j - 1) end
	 if j + 1 < last then quick_sort_range(j + 1, last) end
	 debug ("Recursion")
	    print("Exiting quick_sort_range(")
	    print(first); print(','); print(last); print(")%N")
	 end -- debug
      ensure sorted: is_sorted_range(first, last)
      end -- quick_sort_range