Linked List Example

-- Class APPLICATION
note
    description : "project application root class"
    date        : "$Date$"
    revision    : "$Revision$"

class
    APPLICATION

inherit
    ARGUMENTS

create
    make

feature {NONE} -- Initialization

    make
        local
            list:MY_LINKED_LIST
        do
            create list.make_with (5)
            list.add (3)
            list.add (7)
            list.add (19)
            list.add (1)
            list.add (563)
            io.put_integer (list.ith (3))
            io.new_line
            list.remove_ith (3)
            io.put_integer (list.ith (3))
            io.new_line
            list.add_ith (3, 99)
            io.put_integer (list.ith (3))
            io.new_line
            list.add_ith (1, 88)
            io.put_integer (list.ith (1))
            io.new_line
        end

end


-- Class MY_LINKED_LIST

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

class
    MY_LINKED_LIST

create
    make_with

feature {NONE} -- Initialization

    make_with (i:INTEGER)
            -- Initialization for `Current'.
        do
            create first.set_value(i)
            last := first
        end

feature

    add (i:INTEGER)
            -- add integer at end of list
        local
            new:MY_LINKABLE
        do
            create  new.set_value(i)
            last.set_next(new)
            last := new
        ensure
            length_correct:old length + 1= length
        end

    length: INTEGER
            -- returns lenght of current list
        local
            item:MY_LINKABLE
            i:INTEGER
        do
            from
                item := first
                i := 1
            until
                item.next = void
            loop
                item := item.next
                i := i + 1
            end

            result := i
        end

    remove_ith(i:INTEGER)
            -- removes ith item of the list
        require
            in_range:i > 0 and i <= length

        local
            len:INTEGER

        do
            len := current.length
            if
                i = 1
            then
                first := first.next

            else
                if
                    i = len
                then
                    ith_intern(i-1).set_next(void)
                    last := ith_intern(i-1)
                else
                    ith_intern(i-1).set_next(ith_intern(i+1))
                end
            end

        ensure
            length_correct:old length - 1 = length
            first_adapted: i = 1 implies old ith_intern(2) = first
            last_adapted: i = length implies old ith_intern(length - 1) = last
        end

    ith(i:INTEGER):INTEGER
            -- return value of ith item
        require
            in_range:i > 0 and i <= length
        do
            result := ith_intern(i).value
        end

    add_ith(i,value:INTEGER)
            -- add new linkable at ith position
        require
            in_range: i>0 and i<=length

        local
            new: MY_LINKABLE

        do
            create new.set_value (value)
            if
                i = 1
            then
                new.set_next (first)
                first := new
            else
                new.set_next (ith_intern(i))
                ith_intern(i-1).set_next(new)
            end

        ensure
            length_correct:old length + 1= length

        end


    first, last:MY_LINKABLE

feature {NONE}
    ith_intern(i:INTEGER):MY_LINKABLE
            -- returns value at ith position
            require
                in_range:i > 0 and i <= length
            local
                item:MY_LINKABLE
                count:INTEGER
            do
                from
                    count := 1
                    item := first
                until
                    count >= i
                loop
                    item := item.next
                    count := count + 1
                variant
                    i - count
                end
                result := item
            end

invariant
    first_equals_last: length = 1 implies first = last
    first_unequals_last: length /= 1 implies first /= last
end


-- Class MY_LINKABLE

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

class
    MY_LINKABLE

create
    set_value

feature -- Initialization

    set_value(val:INTEGER)
            -- Initialization for `Current'.
        do
            value := val
        end

    set_next(nxt:MY_LINKABLE)
            -- change referenz to next object in list
        do
            next := nxt
        end

    value:INTEGER

    next:MY_LINKABLE
end