indexing
   description: "Encapsulation of access to bounded buffers"
class BUFFER_ACCESS [T]
feature
   put(q: separate BOUNDED_BUFFER [T]; x: T) is
	 -- Insert x into q, waiting until q is not full
      require
	 not_full: not q.full
      do
	 q.put(x)
      ensure
	 not_empty: not q.empty
      end -- put
   remove(q: separate BOUNDED_BUFFER [T]) is
	 -- Remove an element from q, waiting until q is not empty
      require
	 not_empty: not q.empty
      do
	 q.remove
      ensure
	 not_full: not q.full
      end -- remove
   item(q: separate BOUNDED_BUFFER [T]): T is
	 -- The oldest element from q, waiting until q is not empty
      require
	 not_empty: not q.empty
      do
	 Result := q.item
      end -- item
end -- BUFFER_ACCESS [T]