+
Point of view
All features
expanded class REVERSE_COLLECTION_SORTER [X -> COMPARABLE]
features
- von_neuman_line (src: COLLECTION[X], dest: COLLECTION[X], count: INTEGER_32, d_count: INTEGER_32, lower: INTEGER_32, imax: INTEGER_32)
- von_neuman_inner_sort (src: COLLECTION[X], dest: COLLECTION[X], sg1: INTEGER_32, count: INTEGER_32, imax: INTEGER_32)
- heap_repair (c: COLLECTION[X], c_lower: INTEGER_32, first: INTEGER_32, last: INTEGER_32)
- quick_sort_region (c: COLLECTION[X], left: INTEGER_32, right: INTEGER_32)
require
ensure
- not c.is_empty implies c.valid_index(Result)
- c.has(element) implies c.item(Result).is_equal(element)
require
ensure
- c.valid_index(Result) implies gt(c.item(Result), element)
- c.valid_index(Result - 1) implies lte(c.item(Result - 1), element)
- Result.in_range(c.lower, c.upper + 1)
require
- src /= dest
- src.lower = dest.lower
- src.upper = dest.upper
- count >= 1
- d_count = count * 2
- lower = src.lower
- imax = src.upper + 1
ensure
- d_count >= dest.count implies is_sorted(dest)
require
- c /= Void
- c.lower = c_lower
- c_lower <= first
- last <= c.upper