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 interface
	LAMPSORT [G -> COMPARABLE]

create 
	make

feature 

	make (l_a: like a)
		ensure
				a = l_a
	
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
		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

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

	lampsort (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j
				j <= a.upper

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

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

	sort_recursive (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j + 1
				j <= a.upper
	
feature -- array queries

	permutation (a1, a2: like a): BOOLEAN
		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 -- class LAMPSORT

Generated by ISE EiffelStudio