Insertion sort (Eiffel)

From LiteratePrograms

This is a simple example of the "insertion sort" sorting algorithm, written in Eiffel.

Overview

Insertion sort works by working progressively through a list or array and inserting each element in turn into its proper place in the already sorted lost or array.

This implementation uses Eiffel generic facilities to enable sorting of arrays of elements of any type that inherits from COMPARABLE, providing flexibility while ensuring that comparison operators are meaningful.

Insertion Sort

<<insertion sort>>=
    insertion_sort (a: ARRAY[X]) is
        require
            a_not_void: a /= Void
        local
            i, j: INTEGER
            value: X
        do
            from
                i := a.lower + 1
            until
                i > a.upper
            loop
                value := a [i]
                from
                    j := i - 1
                until
                    j < a.lower or else a [j] <= value
                loop
                    a [j + 1] := a [j]
                    j := j - 1
                end
                a [j + 1] := value
                i := i + 1
            end
        ensure
            same_count: a.count = old a.count
            sorted: is_sorted (a, a.lower, a.upper)
        end

Correctness

Eiffel supports Design by Contract, here taking the form of pre- and post-conditions requiring that the input array be non-empty, and ensuring that the resulting array has the same number of elements and is sorted. These contracts are converted into runtime checks after compilation for debugging, or can be turned off for finalised code. We do, however, require a definition of a routine to determine whether the array is sorted:

<<is_sorted>>=
is_sorted (a: ARRAY[X]; min, max: INTEGER): BOOLEAN
    require
        a_not_void: a /= Void
        min_valid: a.valid_index (min)
        max_valid: a.valid_index (max)
    local
        i: INTEGER
    do
        Result := True
        from 
            i := min
        invariant
            a.valid_index (i)
        until
            i >= max or not Result
        loop
            Result := a [i] <= a [i + 1]
            i := i + 1
        end
    end

Class declaration

As Eiffel is a fully object-oriented language we must package these routines as features of a class.

<<insertion_sort.e>>=
class INSERTION_SORT [X -> COMPARABLE]
feature -- Sorting
    insertion sort
feature -- Status report
    is_sorted
end

Testing

To test the INSERTION_SORT class we can construct a simple test class demonstrating a run over an array of integers, then over an array of strings.

<<insertion_sort_test.e>>=
class INSERTION_SORT_TEST
create
    make
feature -- Initialization
    make is
        local
            i: INTEGER
            testarray_numeric: ARRAY [INTEGER_8]
            testarray_string: ARRAY [STRING]
            sorter_numeric: INSERTION_SORT [INTEGER_8]
            sorter_string: INSERTION_SORT [STRING]
        do
            create sorter_numeric
            create sorter_string
            testarray_numeric := <<3,8,0,6,7,4,2,1,9,3,1,8,3,9,2,0,9,
                                   4,6,3,0,5,7,9,3,2,5,7,9,0,1,9,3,1>>
            sorter_numeric.insertion_sort (testarray_numeric)
            from
                i := testarray_numeric.lower
            until
                i >= testarray_numeric.upper
            loop
                io.put_integer (testarray_numeric [i])
                io.put_string (",")
                i := i + 1
            end
            io.put_integer (testarray_numeric [i])
            io.put_new_line
            testarray_string := <<"Paris","London","Stockholm","Berlin","Oslo",
                               "Rome","Madrid","Tallinn","Amsterdam","Dublin">>
            sorter_string.insertion_sort (testarray_string)
            from
                i := testarray_string.lower
            until
                i >= testarray_string.upper
            loop
                io.put_string (testarray_string [i])
                io.put_string (",")
                i := i + 1
            end
            io.put_string (testarray_string [i])
            io.put_new_line            
        end
end