class SV_LIST create make, make_from_array feature -- Constant parameters Max_count: INTEGER = 20 N: INTEGER = 5 feature -- Basic API -- Sequence of integers represented as an array sequence: ARRAY [INTEGER] -- Is `sequence' empty? empty: BOOLEAN do Result := (count = 0) ensure Result = (count = 0) end -- Is `k' a position within the bounds of `sequence'? in_bound (k: INTEGER): BOOLEAN do ensure end -- Element at position `k' in `sequence' at (k: INTEGER): INTEGER require do ensure end -- Write `val' at position `k' in `sequence' put (k: INTEGER; val: INTEGER) require in_bound (k) do -- something ensure sequence [k] = val end -- Number of elements stored in `sequence' count: INTEGER require do ensure end feature -- Sorting -- Sort `sequence' sort do if count >= Max_count // 2 and small_elements then bucket_sort (sequence) else merge_sort (sequence, 1, count) end end feature {NONE} -- Sort implementations -- Sort `a' between `low' and `high' using Merge Sort merge_sort (a: ARRAY [INTEGER]; low, high: INTEGER) require do ensure end -- Return a merged copy of `a' [`low'..`mid'] and `a'[`mid' + 1.. `high'] merge (a: ARRAY [INTEGER]; low, mid, high: INTEGER): ARRAY [INTEGER] require do ensure end -- Sort `a' using Bucket Sort bucket_sort (a: ARRAY [INTEGER]) require do ensure end feature {NONE} -- Initialization -- Initialize `sequence' to an empty list make do create sequence.make_empty ensure count = 0 end -- Initialize `sequence' to the content of `a' make_from_array (a: ARRAY [INTEGER]) require attached a a.count <= Max_count do create sequence.make_from_array (a) ensure count = a.count sequence.is_equal (a) end invariant -- `sequence' is a valid reference (not Void) attached sequence -- No more than Max_count elements are ever stored 0 <= count and count <= Max_count end