note
	description: "[
		Quicksort according to Lamport/Meyer.
		The Lampsort algorithm is a simple loop; it does not use recursion, 
		but relies on an interesting data structure, a set of intervals. 
		It is hardly more difficult to understand, 
		and hardly shorter, than the traditional recursive version.
		the recursive version, and its parallelized variants, 
		are only examples of possible implementations
	]"
	author: "JSO"
	date: "$Date$"
	revision: "$Revision$"

class 
	LAMPSORT [G -> COMPARABLE]

create 
	make

feature 

	make (l_a: like a)
		do
			a := l_a
			create picked.make (0, -1)
		ensure
				a = l_a
		end
	
feature 

	a: ARRAY [G]

	pivot1: INTEGER_32

	pivot2: INTEGER_32

	picked: INTEGER_INTERVAL

	partition (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j
				j <= a.upper
		local
			m, n, k: INTEGER_32
			x: G
		do
			from
				x := a [i]
				n := j + 1
				m := i
				k := m
			invariant
					i <= m and m <= k and k <= n and n <= j + 1
					across
						i |..| (m - 1) as it
					all
						a [it.item] < x
					end
					across
						m |..| (k - 1) as kt
					all
						a [kt.item] = x
					end
					across
						n |..| j as jt
					all
						x < a [jt.item]
					end
			variant
					n - k
			until
				k = n
			loop
				if a [k] = x then
					k := k + 1
				elseif a [k] < x then
					swap (m, k)
					m := m + 1
					k := k + 1
				else
					check
							x < a [k]
					end
					swap (k, n - 1)
					n := n - 1
				end
			end
			pivot1 := m - 1
			pivot2 := n
		ensure
				i - 1 <= pivot1 and pivot1 <= j
				i <= pivot2 and pivot2 <= j + 1
				permutation (a, a.deep_twin)
				across
					i |..| pivot1 as it
				all
					across
						(pivot1 + 1) |..| j as jt
					all
						a [it.item] <= a [jt.item]
					end
				end
				across
					i |..| (pivot2 - 1) as it
				all
					across
						pivot2 |..| j as jt
					all
						a [it.item] <= a [jt.item]
					end
				end
		end

	swap (m, n: INTEGER_32)
		require
				a.lower <= m
				m <= n
				n <= a.upper
		local
			temp: G
		do
			temp := a [m]
			a [m] := a [n]
			a [n] := temp
		ensure
				a [m] ~ old a [n] and a [n] ~ old a [m]
		end

	lampsort (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j
				j <= a.upper
		local
			l_intvl: INTEGER_INTERVAL
			intervals: SET [INTEGER_INTERVAL]
		do
			from
				create l_intvl.make (a.lower, a.upper)
				create intervals.make_empty
				intervals.extend (l_intvl)
			invariant
					True
			until
				intervals.is_empty
			loop
				intervals.choose_item
				picked := intervals.item
				intervals.remove_item
				if picked.count > 1 then
					partition (picked.lower, picked.upper)
					intervals.extend (picked.lower |..| pivot1)
					intervals.extend (pivot2 |..| picked.upper)
				end
			end
		end

	sort
			-- Lampsort version of quicksort for array a
		do
			lampsort (a.lower, a.upper)
		ensure
				across
					a.lower |..| (a.upper - 1) as k
				all
					a [k.item] <= a [k.item + 1]
				end
				permutation (old a.deep_twin, a)
		end

	sort2
			-- recursive quicksort
		do
			sort_recursive (a.lower, a.upper)
		ensure
				across
					a.lower |..| (a.upper - 1) as k
				all
					a [k.item] <= a [k.item + 1]
				end
				permutation (old a.deep_twin, a)
		end

	sort_recursive (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j + 1
				j <= a.upper
		do
			if i < j then
				partition (i, j)
				sort_recursive (i, pivot1)
				sort_recursive (pivot2, j)
			end
		end
	
feature -- array queries

	permutation (a1, a2: like a): BOOLEAN
		do
			if a1.count = a2.count then
				Result := across
					a1 as it
				all
					a1.occurrences (it.item) = a2.occurrences (it.item)
				end
			else
				Result := False
			end
		ensure
				Result implies a1.count = a2.count and then across
					a1 as it
				all
					a1.occurrences (it.item) = a2.occurrences (it.item)
				end
				not Result implies a1.count /= a2.count or else (across
					a1 as it
				some
					a1.occurrences (it.item) /= a2.occurrences (it.item)
				end)
		end
	
end -- class LAMPSORT

Generated by ISE EiffelStudio