note
	description	: "Objects that implement bounded buffers."
	author		: "Volkan Arslan, Yann Mueller, Piotr Nienaltowski."
	date		: "$Date: 18.05.2007$"
	revision	: "1.0.0"

class
	BOUNDED_BUFFER [G -> ANY create default_create end]

create
	make_with_capacity

feature -- Initialization

	make_with_capacity (a_capacity: INTEGER)
			-- Initialize with capacity of `a_capacity'.
		require
			valid_capacity: a_capacity > 0
		do
			create storage.make
			capacity := a_capacity
		ensure
			capacity_set: capacity = a_capacity
			empty: is_empty
		end

feature -- Access

	last_consumed_item: detachable G
			-- Last item removed by `consume'.
		note
			option: stable
		attribute
		end

feature -- Element change

	put (a_element: G)
			-- Store element.
		require
			not_full: not is_full
		do
			storage.extend (a_element)
			print ("%NBUFFER: added element " + a_element.out)
		ensure
			count_incremented: count = old count + 1
			not_empty: not is_empty
		end

	consume
			-- Consume an element.
		require
			not_empty: not is_empty
		do
			last_consumed_item := storage.first
			storage.start
			storage.remove
			print ("%NBUFFER: removing element " + last_consumed_item.out + ".")
		ensure
			count_decremented: count = old count - 1
			not_full: not is_full
		end

feature -- Status report

	is_full: BOOLEAN
			-- Is buffer full?
		do
			Result := (storage.count = capacity)
		ensure
			correct_result: Result = (storage.count = capacity)
		end

	is_empty: BOOLEAN
			-- Is buffer empty?
		do
			Result := storage.count = 0
		ensure
			correct_result: Result = (storage.count = 0)
		end

feature -- Measurement

	capacity: INTEGER
		-- Maximum number of elements.

	count: INTEGER
			-- The number of elements.
		do
			Result := storage.count
		ensure
			correct_result: Result = storage.count
		end

feature {NONE}-- Implementation

	storage: LINKED_LIST [G]
			-- Implementation.

invariant
	capacity_positive: capacity > 0
	correct_count: storage.count <= capacity

end -- class BOUNDED_BUFFER