note
	description: "[
			Container where all elements are unique with respect to object equality. 
			Elements can be added and removed.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: set, lock
	manual_inv: true
	false_guards: true

deferred class
	V_SET [G -> ANY]

inherit
	V_CONTAINER [G]
		rename
			has as has_exactly
		redefine
			count,
			is_empty,
			occurrences,
			is_model_equal
		end

	V_LOCKER [G]
		rename
			locked as set
		redefine
			set,
			is_model_equal
		end

feature -- Measurement

	count: INTEGER
			-- Number of elements.
		deferred
		ensure then
			definition_set: Result = set.count
		end

feature -- Status report

	is_empty: BOOLEAN
			-- Is container empty?
		note
			status: nonvariant
		do
			check inv end
			Result := count = 0
		ensure then
			definition_set: Result = set.is_empty
		end

feature -- Search

	has (v: G): BOOLEAN
			-- Is `v' contained?
			-- (Uses object equality.)
		require
			v_closed_with_subjects: v.is_closed_with_subjects
			lock_closed: lock.closed
		deferred
		ensure
			definition: Result = set_has (v)
		end

	item (v: G): G
			-- Element of `set' equivalent to `v' according to object equality.
		require
			v_closed_with_subjects: v.is_closed_with_subjects
			has: set_has (v)
			lock_closed: lock.closed
		deferred
		ensure
			definition: Result = set_item (v)
		end

	occurrences (v: G): INTEGER
			-- How many times is `v' contained?
			-- (Uses reference equality.)
		note
			status: impure, nonvariant
		do
			if has_exactly (v) then
				Result := 1
			end
			check inv end
		end

feature -- Iteration

	new_cursor: V_SET_ITERATOR [G]
			-- New iterator pointing to a position in the set, from which it can traverse all elements by going `forth'.
		note
			status: impure
		deferred
		end

	at (v: G): V_SET_ITERATOR [G]
			-- New iterator over `Current' pointing at element `v' if it exists and `after' otherwise.
		note
			status: impure
		require
			lock_wrapped: lock.is_wrapped
			v_locked: lock.locked [v]
		deferred
		ensure
			result_fresh: Result.is_fresh
			result_wrapped: Result.is_wrapped and Result.inv
			result_in_observers: observers = old observers & Result
			target_definition: Result.target = Current
			index_definition_found: set_has (v) implies Result.sequence [Result.index_] = set_item (v)
			index_definition_not_found: not set_has (v) implies Result.index_ = Result.sequence.count + 1
			modify_field (["observers", "closed"], Current)
		end

feature -- Comparison

	is_subset_of (other: V_SET [G]): BOOLEAN
			-- Does `other' have all elements of `Current'?
			-- (Uses object equality.)
		note
			status: impure, nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: other.lock = lock
		local
			it: like new_cursor
		do
			Result := True
			if other /= Current then
				from
					it := new_cursor
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					inv_only ("lock_non_current", "items_locked")
					other.inv_only ("items_locked")
					lock.inv_only ("owns_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					Result implies ∀ i: 1 |..| (it.index_ - 1) ¦ other.set_has (it.sequence [i])
					not Result implies not other.set_has (it.sequence [it.index_ - 1])
					modify_model ("index_", it)
				until
					it.after or not Result
				loop
					if attached it.item as v then
						Result := other.has (v)
					else
						check from_loop_exit_condition: False then end
					end
					it.forth
				variant
					it.sequence.count - it.index_
				end
				forget_iterator (it)
			end
			check inv_only ("locked_non_void") end
		ensure
			definition: Result = ∀ x: set ¦ other.set_has (x)
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("observers", [Current, other])
		end

	is_superset_of (other: V_SET [G]): BOOLEAN
			-- Does `Current' have all elements of `other'?
			-- (Uses object equality..)
		note
			status: impure, nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: other.lock = lock
		do
			Result := other.is_subset_of (Current)
		ensure
			definition: Result = ∀ x: other.set ¦ set_has (x)
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("observers", [Current, other])
		end

	disjoint (other: V_SET [G]): BOOLEAN
			-- Do no elements of `other' occur in `Current'?
			-- (Uses object equality.)
		note
			status: impure, nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: other.lock = lock
		local
			it: like new_cursor
		do
			if other.is_empty then
				Result := True
			elseif other /= Current then
				from
					it := new_cursor
					Result := True
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					inv_only ("lock_non_current", "items_locked")
					other.inv_only ("items_locked")
					lock.inv_only ("owns_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					Result implies ∀ i: 1 |..| (it.index_ - 1) ¦ not other.set_has (it.sequence [i])
					not Result implies other.set_has (it.sequence [it.index_ - 1])
					modify_model ("index_", it)
				until
					it.after or not Result
				loop
					if attached it.item as v then
						Result := not other.has (v)
					else
						check from_loop_exit_condition: False then end
					end
					it.forth
				variant
					it.sequence.count - it.index_
				end
				forget_iterator (it)
			end
			check inv_only ("locked_non_void") end
		ensure
			definition: Result = ∀ x: set ¦ not other.set_has (x)
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("observers", [Current, other])
		end

feature -- Extension

	extend (v: G)
			-- Add `v' to the set.
		require
			v_locked: lock.locked [v]
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		deferred
		ensure
			abstract_effect: set_has (v)
			precise_effect_has: old set_has (v) implies set = old set
			precise_effect_new: not old set_has (v) implies set = old set & v
			modify_model ("set", Current)
		end

	join (other: V_SET [G])
			-- Add all elements from `other'.
		note
			status: nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: other.lock = lock
			no_iterators: observers.is_empty
		local
			it: V_SET_ITERATOR [G]
		do
			check inv_only ("locked_non_void") end
			if other /= Current then
				from
					it := other.new_cursor
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					inv_only ("lock_non_current", "items_locked")
					other.inv_only ("lock_non_current", "items_locked")
					lock.inv_only ("owns_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					set.old_ <= set
					∀ i: 1 |..| (it.index_ - 1) ¦ set_has (it.sequence [i])
					∀ x: set ¦ set.old_ [x] or other.set.old_ [x]
					modify_model ("set", Current)
					modify_model ("index_", it)
				until
					it.after
				loop
					extend (it.item)
					it.forth
				variant
					it.sequence.count - it.index_
				end
				other.forget_iterator (it)
			end
		ensure
			has_old: old set <= set
			has_other: ∀ y: old other.set ¦ set_has (y)
			no_extra: ∀ x: set ¦ set.old_ [x] or other.set.old_ [x]
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("set", Current)
			modify_model ("observers", [Current, other])
		end

feature -- Removal

	remove (v: G)
			-- Remove `v' from the set, if contained.
			-- Otherwise do nothing.
		note
			status: nonvariant
		require
			v_locked: lock.locked [v]
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		local
			it: like new_cursor
		do
			check inv_only ("lock_non_current", "items_locked", "no_duplicates") end
			check lock.inv_only ("owns_definition", "equivalence_definition") end
			it := at (v)
			if not it.after then
				v.lemma_transitive (it.sequence [it.index_], set / it.sequence [it.index_])
				it.remove
				check it.inv end
			end
			forget_iterator (it)
		ensure
			abstract_effect: not set_has (v)
			precise_effect_not_found: not old set_has (v) implies set = old set
			precise_effect_found: old set_has (v) implies set = old (set / set_item (v))
			observers_restored: observers ~ old observers
			modify_model (["set", "observers"], Current)
		end

	meet (other: V_SET [G])
			-- Keep only elements that are also in `other'.
		note
			status: nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: lock = other.lock
			no_iterators: observers.is_empty
		local
			it: like new_cursor
		do
			check inv_only ("locked_non_void") end
			if other /= Current then
				from
					it := new_cursor
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					it.inv
					inv_only ("lock_non_current", "items_locked", "no_duplicates")
					other.inv_only ("lock_non_current", "items_locked")
					lock.inv_only ("owns_definition", "equivalence_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					set <= set.old_
					∀ i: 1 |..| (it.index_ - 1) ¦ attached it.sequence [i] as x and then other.set_has (x)
					∀ y: set.old_ ¦ other.set_has (y) implies set [y]
					modify_model ("set", Current)
					modify_model (["sequence", "index_"], it)
				until
					it.after
				loop
					if not other.has (it.item) then
						it.remove
					else
						it.forth
					end
				variant
					it.sequence.count - it.index_
				end
				forget_iterator (it)
			end
		ensure
			only_old: set <= old set
			not_too_few: ∀ y: old set ¦ other.set_has (y).old_ = set_has (y)
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("set", Current)
			modify_model ("observers", [Current, other])
		end

	subtract (other: V_SET [G])
			-- Remove elements that are in `other'.
		note
			status: nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: lock = other.lock
			no_iterators: observers.is_empty
		local
			it: V_SET_ITERATOR [G]
		do
			check inv_only ("locked_non_void") end
			if other /= Current then
				from
					it := other.new_cursor
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					inv_only ("lock_non_current", "items_locked", "no_duplicates")
					other.inv_only ("lock_non_current", "items_locked")
					lock.inv_only ("owns_definition", "equivalence_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					set <= set.old_
					∀ i: 1 |..| (it.index_ - 1) ¦ attached it.sequence [i] as x implies not set_has (x)
					∀ y: set.old_ ¦ not other.set_has (y) implies set [y]
					observers ~ observers.old_
					modify_model (["set", "observers"], Current)
					modify_model ("index_", it)
				until
					it.after
				loop
					remove (it.item)
					it.forth
				variant
					it.sequence.count - it.index_
				end
				other.forget_iterator (it)
			else
				wipe_out
			end
		ensure
			only_old: set <= old set
			not_too_few: ∀ y: old set ¦ other.set_has (y).old_ /= set_has (y)
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("set", Current)
			modify_model ("observers", [Current, other])
		end

	symmetric_subtract (other: V_SET [G])
			-- Keep elements that are only in `Current' or only in `other'.
		note
			status: nonvariant
		require
			lock_wrapped: lock.is_wrapped
			same_lock: lock = other.lock
			no_iterators: observers.is_empty
		local
			it: V_SET_ITERATOR [G]
			seq: MML_SEQUENCE [G]
		do
			check inv_only ("locked_non_void", "lock_non_current") end
			if other /= Current then
				from
					it := other.new_cursor
					seq := it.sequence
					check other.inv_only ("locked_non_void", "lock_non_current", "bag_definition") end
				invariant
					is_wrapped
					it.is_wrapped
					inv_only ("items_locked")
					other.inv_only ("items_locked")
					lock.inv_only ("owns_definition")
					1 <= it.index_ and it.index_ <= seq.count + 1
					∀ x: set.old_ ¦ other.set_has (x).old_ or set [x]
					∀ j: 1 |..| (it.index_ - 1) ¦ lock.set_has (set.old_, seq [j]) or set [seq [j]]
					∀ x: set ¦ set.old_ [x] or ∃ j: 1 |..| (it.index_ - 1) ¦ x = seq [j]
					observers ~ observers.old_
					modify_model (["set", "observers"], Current)
					modify_model ("index_", it)
				until
					it.after
				loop
					if attached it.item as v then
						if has (v) then
							check it.inv_only ("target_bag_constraint") end
							seq.lemma_no_duplicates
							check other.inv_only ("items_locked", "no_duplicates") end
							check inv_only ("items_locked", "no_duplicates") end
							check lock.inv_only ("equivalence_definition") end
							remove (v)
						else
							extend (v)
						end
					else
						check from_loop_exit_condition: False then end
					end
					it.forth
				variant
					seq.count - it.index_
				end
				other.forget_iterator (it)
			else
				wipe_out
			end
		ensure
			set_effect_old: ∀ x: old set ¦ other.set_has (x).old_ or set [x]
			set_effect_other: ∀ x: other.set.old_ ¦ set_has (x).old_ or set [x]
			set_effect_new: ∀ x: set ¦ set.old_ [x] or other.set.old_ [x]
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("set", Current)
			modify_model ("observers", [Current, other])
		end

	wipe_out
			-- Remove all elements.
		require
			no_iterators: observers.is_empty
		deferred
		ensure
			set_effect: set.is_empty
			modify_model ("set", Current)
		end

feature -- Specification

	set: MML_SET [G]
			-- Set of elements.
		note
			status: ghost
			replaces: bag
		attribute
			check is_executable: False then end
		end

	set_has (v: G): BOOLEAN
			-- Does `set' contain an element equal to `v' under object equality?
		note
			status: ghost, functional, nonvariant
		require
			lock_exists: lock /= Void
			v_exists: v /= Void
			set_non_void: set.non_void
			reads_field (["set", "lock"], Current)
			reads (set, v)
		do
			Result := lock.set_has (set, v)
		end

	set_item (v: G): G
			-- Element of `set' that is equal to `v' under object equality.
		note
			status: ghost, functional, nonvariant
		require
			lock_exists: lock /= Void
			v_exists: v /= Void
			v_in_set: set_has (v)
			set_non_void: set.non_void
			reads_field (["set", "lock"], Current)
			reads (set, v)
		do
			Result := lock.set_item (set, v)
		end

	bag_from (s: like set): like bag
			-- A bag that contains all elements of `s' exactly once.
		note
			status: ghost, nonvariant, static
			explicit: contracts
		require
			reads ([])
		local
			x: G
			s1: like set
		do
			from
				s1 := s
				create Result
			invariant
				s = s1 + Result.domain
				s1.is_disjoint (Result.domain)
				Result.is_constant (1)
				s.count = s1.count + Result.count
				decreases (s1)
			until
				s1.is_empty
			loop
				x := s1.any_item
				Result := Result & x
				s1 := s1 / x
			end
		ensure
			Result.domain = s
			Result.count = s.count
			Result.is_constant (1)
		end

	is_model_equal (other: like Current): BOOLEAN
			-- Is the abstract state of `Current' equal to that of `other'?
		note
			status: ghost, functional, nonvariant
		do
			Result := set ~ other.set
		end

invariant
	bag_definition: bag = bag_from (set)

note
	copyright: "Copyright (c) 1984-2021, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
			Eiffel Software
			5949 Hollister Ave., Goleta, CA 93117 USA
			Telephone 805-685-1006, Fax 805-685-6869
			Website http://www.eiffel.com
			Customer support http://support.eiffel.com
		]"

end