SET_INT

note
    description: "{SET_INT} implements a set of integers"

class
    SET_INT
inherit
    ANY
    redefine
        out
    end
create
    empty_set, singleton

feature {NONE} -- Initialization
    empty_set
        do
            create elements.make
            elements.start
        end
    singleton (element : INTEGER)
        do
            empty_set
            elements.force (element)
        end

feature -- Queries

    is_empty: BOOLEAN
            -- Is the current set empty?
        do
            Result := elements.is_empty
        ensure
            result_correct : Result implies elements.count = 0
        end

    has (v: INTEGER): BOOLEAN
            -- Does the Current set have 'v'?
        local
            i : INTEGER
        do
            from
                i := 1
            until
                i > elements.count
            loop
                if v ~ elements @ i then
                    Result := True
                end
                i := i + 1
            variant
                elements.count - i + 1
            end
        ensure
            Result = (across 1 |..| card as ith some elements [ith.item] = v end)
        end

    card: INTEGER
            -- What is the cardinality of the Current set?
        do
            Result := elements.count
        ensure
            result_correct: Result = elements.count
        end

    is_subset (other: SET_INT): BOOLEAN
            -- Is the Current set a subset of 'other'?
        do
            Result := True
            from
                elements.start
            until
                elements.exhausted
            loop
                if not other.has (elements.item) then
                    Result := False
                end
                elements.forth
            end
        ensure
            result_correct : elements.count = 0 or across other.elements as element all other.has (element.item) end
        end

    is_not_subset (other: SET_INT): BOOLEAN
            -- Is the Current set not a subset of 'other'?
        local
            i : INTEGER
        do
            Result := False
            from
                elements.start
            until
                elements.exhausted
            loop
                if not other.has (elements.item) then
                    Result := True
                end
                elements.forth
            variant
                elements.count - elements.index
            end

        ensure
            result_correct: across elements as element some not other.has (element.item) end
        end

    is_strict_subset (other: SET_INT): BOOLEAN
            -- Is the Current set a strict subset of 'other'?
        do
            Result := Current.is_subset (other) and not other.is_subset (Current)
        ensure
            result_correct: across other.elements as element some not Current.has (element.item) end
        end

    is_not_strict_subset (other: SET_INT): BOOLEAN
            -- Is the Current set not a strict subset of 'other'?
        do
            Result := Current.is_subset (other)
        ensure
            result_correct: across elements as element all other.has (element.item) end
        end

    min: INTEGER
            -- gives the smallest number in the current set
        require
            at_least_one_element: not is_empty
        do
            from
                elements.start
                Result := elements.item
                elements.forth
            until
                elements.exhausted
            loop
                if elements.item <  Result then
                    Result := elements.item
                end
            end

        ensure
            result_correct: across elements as element all element.item >= Result end
        end

    max: INTEGER
            -- gives the largest number in the current set
        require
            at_least_one_element: not is_empty
        do
            from
                elements.start
                Result := elements.item
                elements.forth
            until
                elements.exhausted
            loop
                if elements.item > Result then
                        Result := elements.item
                end
        end
        ensure
            result_correct: across elements as element all element.item <= Result end
        end

    equal_set (other: SET_INT): BOOLEAN
            -- Is Current set equal to other?
        do
            Result := Current.is_subset (other) and other.is_subset (current)
        ensure
            equal_sets: Result = is_subset (other) and then other.is_subset (Current)
        end


feature -- Modification

    add (v: INTEGER)
            -- adds an element to the set
        do
            if not Current.has (v) then
                elements.force (v)
            end
        ensure
            element_in_set: has (v)
        end

feature -- Operations (no side effect)
    union (other: SET_INT): SET_INT
            -- gives the union of the elements of other and Current
        do
            create Result.empty_set
            Result.elements.copy (elements)
            from
                other.elements.start
            until
                other.elements.exhausted
            loop
                if not Result.has (other.elements.item) then
                    Result.add (other.elements.item)
                end
                other.elements.forth
            end
        ensure
            union_correct: Current.is_subset (Result) and other.is_subset (Result)
        end

    intersection (other: SET_INT): SET_INT
            -- gives the intersection of the elements of other and Current
        do
            create Result.empty_set
            from
                elements.start
            until
                elements.exhausted
            loop
                if other.has (elements.item) then
                    Result.add (elements.item)
                end
                elements.forth
            end
        ensure
            result_correct: across Result.elements as element all Current.has (element.item) and other.has (element.item) end
        end

    difference alias "-"(other: SET_INT): SET_INT
            -- gives the difference of the elements of Current and other
        do
            create Result.empty_set
            from
                elements.start
            until
                elements.exhausted
            loop
                if not other.has (elements.item) then
                    Result.add (elements.item)
                end
                elements.forth
            end
        ensure
            result_correct: across elements as element all not other.has (element.item) implies Result.has (element.item) end
        end

    out: STRING
            -- Returns a printable set
        local
            index: INTEGER
        do
            Result := ""
            Result := Result +  ("{")
            from
                index := 1
            until
                index > card
            loop
                Result := Result + elements [index].out
                if index < card then
                    Result := Result + ", "
                end
                index := index + 1
            end
            Result := Result + "}"
        end

feature -- Access

    elements: LINKED_LIST [INTEGER]
            -- `elements' contains the elements of the set


invariant
    no_repeated_elements: across 1 |..| card as ith all elements.occurrences (elements [ith.item]) = 1 end
end