note
    description: "Summary description for {ARRAY_SORTABLE}."
    author: ""
    date: "$Date$"
    revision: "$Revision$"

class
    ARRAY_SORTABLE [G -> COMPARABLE]

inherit
    ARRAY [G]

create
    make

feature -- Sorting

    selection_sort
        -- Sort current area using selection sort algorithm
        local
            i: INTEGER
        do
            from
                i:= lower
            invariant
                valid_index (i) or i = upper + 1
                i /= lower implies is_sorted(lower, i-1)
            variant
                upper - i + 1
            until
                i > upper
            loop
                swap(i, get_minimun_index(i, upper))
                i:=i+1
            end
        ensure
            same_count: old count = count
            stable_lower: lower = old lower
            stable_upper: upper = old upper
            is_sorted(lower,upper)
        end

    get_minimun_index (start_pos, end_pos: INTEGER): INTEGER
        -- Get the index with minor value bounds start_pos and end_pos.
        require
            valid_start_pos: valid_index (start_pos)
            valid_end_pos: end_pos <= upper
            valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
        local
            i: INTEGER
        do
            result := start_pos
            from
                i := start_pos
            invariant
                valid_index (i) or i = end_pos + 1
            variant
                end_pos - i + 1
            until
                i > end_pos
            loop
                if area[i-lower] <= area[result-lower] then
                    result := i;
                end
                i:=i+1
            end
        ensure
            same_count: old count = count
            stable_lower: lower = old lower
            stable_upper: upper = old upper
        end

    swap(index_1: INTEGER; index_2:INTEGER)
        -- Intercambia los valores en el arreglo
        require
            valid_index: valid_index (index_1)
            valid_index: valid_index (index_2)
        local
            aux : G
        do
            aux:= area[index_1-lower]
            area[index_1 - lower] := area[index_2 - lower]
            area[index_2 - lower] := aux
        ensure
            same_count: old count = count
            stable_lower: lower = old lower
            stable_upper: upper = old upper
            old area[index_1 - lower] = area[index_2 - lower]
            old area[index_2 - lower] = area[index_1 - lower]
        end

    is_sorted (start_pos, end_pos: INTEGER): BOOLEAN
        -- Return true if current area is sorted increasingly
        require
            valid_start_pos: valid_index (start_pos)
            valid_end_pos: end_pos <= upper
            valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
        local
            i: INTEGER
        do
            Result := True
            from
                i := start_pos
            invariant
                valid_index (lower + i)
            variant
                end_pos - i + 1
            until
                i = end_pos or not Result
            loop
                Result := ( area[i-lower] <= area[(i - lower) + 1])
                i := i + 1
            end
        end

end