deferred class interface P_TRAVERSABLE[G]

feature(s) from P_CONTAINER
   --  Status

   count: INTEGER
      --  Number of items in the container.

      ensure
         positive: Result >= 0

   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   is_writable: BOOLEAN
      --  Is the structure writable?


   item: G
      --  Current item.

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Remove all objects from the container.

      require
         writable: is_writable
      ensure
         done: is_empty

feature(s) from P_CONTAINER
   --  Output

   out: STRING
      --  String representation.

      ensure
         is_copy:  --  new string

feature(s) from P_CONTAINER
   --  Utility

   is_void (x: ANY): BOOLEAN
      --  Void assertion for generic parameters.


feature(s) from P_ONEWAY_TRAVERSABLE
   --  Iteration

   iterator: P_ITERATOR[G]
      --  Get a two-way iterator on this container.

      ensure
         done: Result /= Void; --  Result /= previous Result
         is_shallow_copy: 

   is_protected: BOOLEAN
      --  Is an iterator inside the data structure?


feature(s) from P_ONEWAY_TRAVERSABLE
   --  Lock status

   has_locked: BOOLEAN
      --  Does this container has one or more locked items?


   is_locked: BOOLEAN
      --  Is the current item locked?

      require
         meaningful: not is_empty
      ensure
         has_locked: Result = true implies has_locked

invariant
   empty: is_empty = count = 0;
   valid_protect_count: protcount >= 0;
   protection: is_protected implies not is_writable;

end of deferred P_TRAVERSABLE[G]