-- Node in a circular doubly-linked list
-- This example demonstrates multi-object invariants and update guards.

frozen class DLL_NODE

create
	make

feature {NONE} -- Initialization

	make
			-- Create a singleton node.
		note
			status: creator
		do
			left := Current
			right := Current
			-- Since `subjects' and `observers' have a simple structure,
			-- they are assigned automatically
		ensure
			singleton: left = Current
		end

feature -- Access

	left: DLL_NODE
			-- Left neighbor.
		note
			-- This update guard lets us update the attribute
			-- without notifying any observer expect `Current.left':
			guard: not_left
		attribute
		end

	right: DLL_NODE
			-- Right neighbor.
		note
			-- This update guard lets us update the attribute
			-- without notifying any observer expect `Current.right':
			guard: not_right
		attribute
		end

feature -- Modification

	insert_right (n: DLL_NODE)
			-- Insert node `n' to the right of the current node.
		note
			explicit: wrapping -- Do not automatically unwrap/wrap `Current'
		require
			n_singleton: n.left = n
			right_wrapped: right.is_wrapped
			modify (Current, right, n)
		local
			r: DLL_NODE
		do
			r := right
			unwrap_all ([Current, r, n])

			n.set_right (r)
			n.set_left (Current)

			r.set_left (n)
			set_right (n)

			n.set_subjects ([r, Current])
			n.set_observers ([r, Current])
			set_subjects ([left, n])
			set_observers ([left, n])
			r.set_subjects ([n, r.right])
			r.set_observers ([n, r.right])
			wrap_all ([Current, r, n])
		ensure
			n_left_set: right = n
			n_right_set: n.right = old right
		end

	remove
			-- Remove the current node from the list.
		note
			explicit: wrapping -- Do not automatically unwrap/wrap `Current'
		require
			right_wrapped: right.is_wrapped
			left_wrapped: left.is_wrapped
			modify (Current, left, right)
		local
			l, r: DLL_NODE
		do
			l := left
			r := right
			unwrap_all ([Current, l, r])

			set_left (Current)
			set_right (Current)

			l.set_right (r)
			r.set_left (l)

			set_subjects ([Current])
			set_observers ([Current])
			l.set_subjects ([l.left, r])
			l.set_observers ([l.left, r])
			r.set_subjects ([l, r.right])
			r.set_observers ([l, r.right])
			wrap_all ([Current, l, r])
		ensure
			singleton: right = Current
			old_left_wrapped: (old left).is_wrapped
			old_right_wrapped: (old right).is_wrapped
			neighbors_connected: (old left).right = old right
		end

feature {DLL_NODE} -- Implementation

	set_left (n: DLL_NODE)
			-- Set left neighbor to `n'.
		require
			open: is_open
			left_open: left.is_open
			modify_field ("left", Current)
		do
			-- According to the update guard of attribute `left',
			-- other observers except `Current.left' cannot be invalidated by this update;
			-- this is why we only require that `Current.left' be open,
			-- and this is why we can perform list insertions and removals opening only three nodes
			-- (see `insert_right' and `remove').
			left := n
		ensure
			left = n
		end

	set_right (n: DLL_NODE)
			-- Set right neighbor to `n'.
		require
			open: is_open
			right_open: right.is_open
			modify_field ("right", Current)
		do
			-- According to the update guard of attribute `right',
			-- other observers except `Current.right' cannot be invalidated by this update;
			-- this is why we only require that `Current.right' be open,
			-- and this is why we can perform list insertions and removals opening only three nodes
			-- (see `insert_right' and `remove').			
			right := n
		ensure
			right = n
		end

feature -- Specification

	not_left (new_left: DLL_NODE; o: ANY): BOOLEAN
			-- Is `o' different from `left'?
		note
			status: functional
		do
			Result := o /= left
		end

	not_right (new_right: DLL_NODE; o: ANY): BOOLEAN
			-- Is `o' different from `right'?
		note
			status: functional
		do
			Result := o /= right
		end

invariant
	left_exists: left /= Void
	right_exists: right /= Void
	subjects_structure: subjects = [ left, right ]
	observers_structure: observers = [ left, right ]
	-- These two invariant clauses depend on the state of other objects.
	-- They are only admissible because `left' and `right' are contained in `subjects'
	-- (try commenting out `subjects_structure' clause to see this).
	left_consistent: left.right = Current
	right_consistent: right.left = Current

end