class interface P_LINKED_ITERATOR[G]

feature(s) from P_ONEWAY_ITERATOR
   --  Copy

   copy (other: like Current)
      --  Cannot copy iterator.

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

feature(s) from P_ONEWAY_ITERATOR
   --  Access

   outside: BOOLEAN
      --  Is the iterator outside the container?


   iterable: BOOLEAN
      --  Is the associated structure iterable (not empty)?


   item: G
      --  Return the item at the current position.

      require
         inside: not outside

feature(s) from P_ONEWAY_ITERATOR
   --  Synchronization

   synchronize_container
      --  Set the current item of the target container to be 
      --  the one currently pointed at by the iterator.
      --  THIS METHOD DOES CHANGE THE CONTAINER STATE.

      require
         inside: not outside
      ensure
         done:  --  container current position changed

feature(s) from P_ONEWAY_ITERATOR
   --  Iteration

   first
      --  Go to first item of the container.

      require
         outside: outside
      ensure
         done: iterable implies not outside

   synchronize
      --  Set the iterator so that the iterator current item is 
      --  the current item of the container. Do not change the 
      --  container. 

      require
         outside: outside;
         iterable: iterable
      ensure
         done: not outside

   forth
      --  Next item.

      require
         inside: not outside

   stop
      --  Finish.

      require
         inside: not outside
      ensure
         done: outside

feature(s) from P_ONEWAY_ITERATOR
   --  Iterator locking

   is_locked: BOOLEAN
      --  Is the current iterator locked?


   lock
      --  Lock iterator: lock the current item into the container 
      --  and leave the iterator.

      require
         inside: not outside;
         unlocked: not is_locked
      ensure
         locked: is_locked;
         outside: outside

   unlock
      --  Unlock iterator

      require
         locked: is_locked;
         outside: outside
      ensure
         inside: not outside;
         not_locked: not is_locked

feature(s) from P_ONEWAY_ITERATOR
   --  Variant support

   forward_variant: INTEGER
      --  Forward variant for forth-only loops.


feature(s) from P_ITERATOR
   --  Iteration

   last
      --  Go to the last item of the container.

      require
         outside: outside
      ensure
         done: iterable implies not outside

   back
      --  Previous item.

      require
         inside: not outside

feature(s) from P_ITERATOR
   --  Variant support

   backward_variant: INTEGER
      --  Forward variant for forth-only loops.


invariant
   outside_locked: not outside implies not is_locked;
   protection: not outside implies container.is_protected;
   valid_node: not outside implies cur_node /= Void;

end of P_LINKED_ITERATOR[G]