deferred class interface P_TREE[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

   linear_iterator: P_ONEWAY_ITERATOR[G]
      --  Get a linear 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

feature(s) from P_TREE
   --  Linear iteration

   preorder_iterator: P_ONEWAY_ITERATOR[G]
      --  Linear preorder iterator.

      ensure
         valid: Result /= Void; --  new iterator provided for each call
         is_shallow_copy: 

   postorder_iterator: P_ONEWAY_ITERATOR[G]
      --  Linear postorder iterator.

      ensure
         valid: Result /= Void; --  new iterator provided for each call
         is_shallow_copy: 

   levelorder_iterator: P_ONEWAY_ITERATOR[G]
      --  Linear level order iterator.

      ensure
         valid: Result /= Void; --  new iterator provided for each call
         is_shallow_copy: 

feature(s) from P_TREE
   --  Modification

   add_left (new: G)
      --  Add an item to the left of current item.

      require
         writable: is_writable;
         has_item: not is_empty;
         not_root: not is_root
      ensure
         count: count = old count + 1;
         keep_reference: item = new

   add_right (new: G)
      --  Add an item to the right of current item.

      require
         writable: is_writable;
         has_item: not is_empty;
         not_root: not is_root
      ensure
         count: count = old count + 1;
         keep_reference: item = new

   add_root (new_root: G)
      --  Add the root item.

      require
         writable: is_writable;
         empty: is_empty
      ensure
         count: count = 1;
         keep_reference: item = new_root;
         root: is_root;
         sole_root: is_top and is_bottom and is_left and is_right

   add_child (new: G)
      --  Add a first child to the current item.
      --  Other children may be added with add_right/add_left

      require
         writable: is_writable;
         has_item: not is_empty;
         down: is_bottom
      ensure
         count: count = old count + 1;
         keep_reference: item = new;
         unique_child: is_left and is_right;
         still_down: is_leaf

   replace (x: G)
      --  Replace current item.

      require
         writable: is_writable;
         has_item: not is_empty
      ensure
         keep_reference: x = item

   remove
      --  Remove current item and its children.
      --  The tree shall not have locked items.

      require
         writable: is_writable;
         has_item: not is_empty;
         unlocked: not has_locked
      ensure
         count: count = old count - 1;
         moved: is_root

feature(s) from P_TREE
   --  Cursor

   is_left: BOOLEAN
      --  Is the current item the first one?

      require
         meaningful: not is_empty

   is_right: BOOLEAN
      --  Is the current item the last one?

      require
         meaningful: not is_empty

   is_top: BOOLEAN
      --  Is root generation?

      require
         meaningful: not is_empty

   is_bottom: BOOLEAN
      --  Has the current item not got any children?

      require
         meaningful: not is_empty

   left
      --  Go backwards one slot.

      require
         meaningful: not is_empty;
         not_left: not is_left

   right
      --  Go forward one item.

      require
         meaningful: not is_empty;
         not_right: not is_right

   up
      --  Go one generation upwards.

      require
         meaningful: not is_empty;
         not_up: not is_top

   down
      --  Go one generation downwards.

      require
         meaningful: not is_empty;
         not_down: not is_bottom
      ensure
         position: is_left

   leftmost
      --  Go to the leftmost sibling.

      require
         meaningful: not is_empty
      ensure
         done: is_left

   rightmost
      --  Go to the rightmost sibling.

      require
         meaningful: not is_empty
      ensure
         done: is_right

   root
      --  Go to root node.

      require
         meaningful: not is_empty
      ensure
         done: is_root

feature(s) from P_TREE
   --  Queries

   depth: INTEGER
      --  Number of level from the root. Root depth is 0.

      require
         has_item: not is_empty
      ensure
         positive: Result >= 0;
         root_zero: is_root implies Result = 0

   is_root: BOOLEAN
      --  Is the current item the root?

      require
         has_item: not is_empty
      ensure
         done: Result = (is_top and is_left and is_right)

   is_leaf: BOOLEAN
      --  Is the current item a leaf (node that has no child)?

      require
         has_item: not is_empty
      ensure
         done: Result = is_bottom

feature(s) from P_TREE
   --  Conversions.

   subtree: like Current
      --  Tree which has current node as root node.

      require
         not_empty: not is_empty
      ensure
         done: Result /= Void and not Result.is_empty; --  New tree, old items.
         is_shallow_copy: 

   siblings_list: P_LIST[G]
      --  List of siblings of current item, including current item.

      require
         not_empty: not is_empty
      ensure
         done: Result /= Void and then not Result.is_empty; --  List is a copy but contains real items.
         is_shallow_copy: 

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

end of deferred P_TREE[G]