class
    SV_LIST

create
	make, make_from_array

feature {NONE} -- Initialization

	make
			-- Initialize `sequence' to an empty list
		note
			status: creator
		do
			create array.make (0)
		ensure
			array.sequence.is_constant (0)
			count = 0
		end

	make_from_array (a: SIMPLE_ARRAY [INTEGER])
			-- Initialize `sequence' to the content of `a'
		note
			status: creator
		require
			attached a
			a.count <= Max_count
		do
			create array.make_from_array (a)
		ensure
			count = a.count
			array.sequence = a.sequence
		end

feature -- Constant parameters

	max_count: INTEGER = 20
			-- Maximum number of elements in the list.

	N: INTEGER = 5
			-- Boundary value for algorithm selection.

feature -- Basic API

	array: SIMPLE_ARRAY [INTEGER]
			-- Sequence of integers represented as an array

	empty: BOOLEAN
			-- Is `array' empty?
		note
			status: functional
		require
			inv
		do
			Result := (count = 0)
		ensure
			Result = (count = 0)
		end

	in_bound (k: INTEGER): BOOLEAN
			-- Is `k' a position within the bounds of `array'?
		do
            -- implementation
		ensure
            -- postconditions
		end

	at (k: INTEGER): INTEGER
			-- Element at position `k' in `array'
		require
            -- preconditions
		do
            -- implementation
		ensure
            -- postconditions
		end

	put (k: INTEGER; val: INTEGER)
			-- Write `val' at position `k' in `array'
		require
			in_bound (k)
		do
            -- implementation
		ensure
			array [k] = val
		end

	extend (val: INTEGER)
			-- Extend `array' with an element `val'
		require
            -- preconditions
		do
			array.force (val, count+1)
		ensure
            -- postconditions
		end

	remove
			-- Remove the last element of `array'
		require
            -- preconditions
		do
			array.remove_at (count)
		ensure
            -- postconditions
		end

	count: INTEGER
			-- Number of elements stored in `array'
		note
			status: functional
		require
			inv
		do
            -- implementation
		ensure
            -- postconditions
		end

feature -- Sorting

	sort
			-- Sort `array'
		do
			if count >= Max_count // 2 and has_small_elements (array) then
				array := bucket_sort (array)
			else
				array := quick_sort (array)
			end
		ensure
			is_sorted (array)
			is_permutation (array.sequence, old array.sequence)
		end

feature -- For use in specifications

	has_small_elements (a: SIMPLE_ARRAY [INTEGER]): BOOLEAN
			-- Are all elements of `a' small (i.e., in the range [-3N..3N])?
		note
			status: functional
		require
			a /= Void
		do
			Result := across a.sequence.domain as i all -3*N <= a.sequence[i.item] and a.sequence[i.item] <= 3*N end
		end

	is_sorted (a: SIMPLE_ARRAY [INTEGER]): BOOLEAN
			-- Is `a' sorted?
		note
			status: functional, ghost
		require
			a /= Void
		do
			-- Result := ??
		end

	is_permutation (a, b: MML_SEQUENCE [INTEGER]): BOOLEAN
			-- Is `a' a permuation of `b'?
		note
			status: functional, ghost
		do
			Result := a.to_bag ~ b.to_bag
		end

feature -- Sort implementations

	concatenate_arrays (a: SIMPLE_ARRAY [INTEGER] b: SIMPLE_ARRAY [INTEGER]): SIMPLE_ARRAY [INTEGER]
			-- return the array comprising the elements of `a' followed by those of `b'
		note
			status: impure
			explicit: contracts
		require
			a.is_wrapped
			b.is_wrapped
		local
			i, j: INTEGER
		do
			create Result.make_from_array (a)
			from
				i := 1
				j := Result.count + 1
			invariant
				Result.is_wrapped
				-- more loop invariants?
			until
				i > b.count
			loop
				Result.force (b.item (i), j)
				i := i + 1
				j := j + 1
			end
		ensure
			Result.is_wrapped
			Result.is_fresh
			-- more postconditions?
		end

	quick_sort (a: SIMPLE_ARRAY [INTEGER]): SIMPLE_ARRAY [INTEGER]
			-- Sort `a' using Quicksort
		note
			status: impure
			explicit: contracts
		require
			a.is_wrapped
			decreases(a.sequence)
			modify([])
		local

		do
            -- note: in loop invariants, you should write X.is_wrapped for
            -- each array X that the loop modifies
		ensure
			Result.is_wrapped
			Result.is_fresh
			-- most postconditions?
		end

	bucket_sort (a: SIMPLE_ARRAY [INTEGER]): SIMPLE_ARRAY [INTEGER]
			-- Sort `a' using Bucket Sort
		note
			status: impure
			explicit: contracts
		require
			a.is_wrapped
			-- more preconditions?
		local

		do
            -- note: in loop invariants, you should write X.is_wrapped for
            -- each array X that the loop modifies
		ensure
			Result.is_wrapped
			Result.is_fresh
			-- more postconditions?
		end

invariant
	array_not_void: attached array
	owns_array: owns = [array]
	array_size_restriction: 0 <= array.sequence.count and array.sequence.count <= Max_count

end