class interface P_HISTORY_LIST[G]

creation
   make

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 this container writable?


   item: G
      --  Current item.

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Reset 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_DISPENSER
   --  Update

   add (it: G)
      --  Add at the end of the list, remove first if too big.

      ensure
         done: count < maximum implies count = old count + 1;
         keep_reference:  --  keep a copy of the item.

   remove
      --  This feature need not be used normally.

      require
         meaningful: not is_empty

feature(s) from P_DISPENSER
   --  Conversion

   to_list: P_LIST[G]
      --  List of elements in container.

      ensure
         valid_result: Result /= Void; --  new list but old items.
         is_shallow_copy: 

feature(s) from P_SEQUENCE
   --  Update

   set_index (i: INTEGER)
      --  Set the current item to the one at position 'idx'.

      require
         not_empty: not is_empty;
         index_low: i >= 1;
         index_up: i <= count

feature(s) from P_SEQUENCE
   --  Status

   index: INTEGER
      require
         not_empty: not is_empty
      ensure
         valid: Result >= 1 and Result <= count

feature(s) from P_HISTORY_LIST
   --  from ANY

   copy (other: like Current)
      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

   is_equal (other: like Current): BOOLEAN
      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

feature(s) from P_HISTORY_LIST
   --  Creation

   make

feature(s) from P_HISTORY_LIST
   --  Properties

   maximum: INTEGER
      --  Max number of item in the container.


   set_maximum (max: INTEGER)
      --  Set the maximum number of item in the container.

      require
         positive: max > 0

invariant
   empty: is_empty = count = 0;
   max: maximum > 0;
   coherent_count: count = container.count;
   count: count <= maximum;

end of P_HISTORY_LIST[G]