class interface STRING
   --
   -- Resizable character STRINGs indexed from 1 to count.
   --

creation
   make (needed_capacity: INTEGER)
      -- Initialize the string to have at least needed_capacity
      -- characters of storage.

      require
         non_negative_size: needed_capacity >= 0
      ensure
         needed_capacity <= capacity;
         empty_string: count = 0

   copy (other: like Current)
      -- Copy other onto Current.

      require
         same_dynamic_type(other)
      ensure
         count = other.count;
         is_equal(other)

   make_empty
      -- Create an empty string.


   make_filled (c: CHARACTER; n: INTEGER)
      -- Initialize string with n copies of c.

      require
         valid_count: n >= 0
      ensure
         count_set: count = n;
         filled: occurrences(c) = count

   from_external (p: POINTER)
      -- Internal storage is set using p (may be dangerous because
      -- the external C string p is not duplicated). Assume p has a 
      -- null character at the end in order to compute the Eiffel 
      -- count. This extra null character is not part of the Eiffel 
      -- STRING. Also consider from_external_copy to choose the most 
      -- appropriate.

      require
         p.is_not_null
      ensure
         capacity = count + 1;
         p = to_external

   from_external_copy (p: POINTER)
      -- Internal storage is set using a copy of p. Assume p has a 
      -- null character at the end in order to compute the Eiffel 
      -- count. This extra null character is not part of the Eiffel 
      -- STRING. Also consider from_external to choose the most 
      -- appropriate.

      require
         p.is_not_null

   make_from_string (model: STRING)
      -- (Here for ELKS compatibility.)
      -- Initialize from the characters of model.
      -- Useful in proper descendants of STRING.

      require
         model /= Void
      ensure
         count = model.count

   blank (nr_blanks: INTEGER)

feature(s) from HASHABLE   hash_code: INTEGER
      -- The hash-code value of Current.

      ensure
         good_hash_value: Result >= 0

feature(s) from COMPARABLE   is_equal (other: like Current): BOOLEAN
      -- Do both strings have the same character sequence?
      -- (Redefined from GENERAL)

      require
         other /= Void
      ensure
         trichotomy: Result = (not (Current < other) and not (other < Current));
         generating_type = other.generating_type implies Result = other.is_equal(Current)

   infix "<" (other: like Current): BOOLEAN
      -- Is Current less than other?

      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other < Current)

   infix "<=" (other: like Current): BOOLEAN
      -- Is Current less than or equal other?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (Current < other or is_equal(other))

   infix ">" (other: like Current): BOOLEAN
      -- Is Current strictly greater than other?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

   infix ">=" (other: like Current): BOOLEAN
      -- Is Current greater than or equal than other?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (other <= Current)

   in_range (lower, upper: like Current): BOOLEAN
      -- Return true if Current is in range [lower..upper]

      ensure
         Result = (Current >= lower and Current <= upper)

   compare (other: like Current): INTEGER
      -- If current object equal to other, 0
      -- if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = -1 = (Current < other);
         greater_positive: Result = 1 = (Current > other)

   three_way_comparison (other: like Current): INTEGER
      -- If current object equal to other, 0
      -- if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = -1 = (Current < other);
         greater_positive: Result = 1 = (Current > other)

   min (other: like Current): like Current
      -- Minimum of Current and other.

      require
         other /= Void
      ensure
         Result <= Current and then Result <= other;
         compare(Result) = 0 or else other.compare(Result) = 0

   max (other: like Current): like Current
      -- Maximum of Current and other.

      require
         other /= Void
      ensure
         Result >= Current and then Result >= other;
         compare(Result) = 0 or else other.compare(Result) = 0

feature(s) from STRING   count: INTEGER
      -- String length which is also the maximum valid index.


   capacity: INTEGER
      -- Capacity of the storage area.


   lower: INTEGER
      -- Minimum index; actually, this is always 1 (this feature is
      -- here to mimic the one of the COLLECTIONs hierarchy).


   upper: INTEGER
      -- Maximum index; actually the same value as count (this
      -- feature is here to mimic the one of the COLLECTION hierarchy).

      ensure
         Result = count

feature(s) from STRING
   -- Creation / Modification:

   make (needed_capacity: INTEGER)
      -- Initialize the string to have at least needed_capacity
      -- characters of storage.

      require
         non_negative_size: needed_capacity >= 0
      ensure
         needed_capacity <= capacity;
         empty_string: count = 0

   make_empty
      -- Create an empty string.


   make_filled (c: CHARACTER; n: INTEGER)
      -- Initialize string with n copies of c.

      require
         valid_count: n >= 0
      ensure
         count_set: count = n;
         filled: occurrences(c) = count

feature(s) from STRING
   -- Testing:

   is_empty: BOOLEAN
      -- Has string length 0?


   item (i: INTEGER): CHARACTER
      -- Character at position i.

      require
         valid_index: valid_index(i)

   infix "@" (i: INTEGER): CHARACTER
      -- Character at position i.

      require
         valid_index: valid_index(i)

   valid_index (i: INTEGER): BOOLEAN
      -- True when i is valid (i.e., inside actual bounds).

      ensure
         definition: Result = (1 <= i and i <= count)

   same_as (other: STRING): BOOLEAN
      -- Case insensitive is_equal.

      require
         other /= Void

   item_code (i: INTEGER): INTEGER
      -- Code of character at position i.

      require
         valid_index: valid_index(i)

   index_of (c: CHARACTER; start_index: INTEGER): INTEGER
      -- Index of first occurrence of c at or after start_index,
      -- 0 if none.
      --
      -- Note: see also first_index_of to start searching at 1.
      -- Actually first_index_of is not exactely the equivalent of 
      -- index_of in release -0.76: when the search failed the result is
      -- now 0 (and no longer count + 1). So, to update your code from
      -- release -0.76 to release -0.75, replace index_of with 
      -- first_index_of and be careful to see what's done with the 
      -- result !

      require
         valid_start_index: start_index >= 1 and start_index <= count + 1
      ensure
         Result /= 0 implies item(Result) = c

   reverse_index_of (c: CHARACTER; start_index: INTEGER): INTEGER
      -- Index of first occurrence of c at or before start_index,
      -- 0 if none.
      --
      -- Note: search is done in reverse direction, which means 
      -- from the index down to the first character.

      require
         valid_start_index: start_index >= 0 and start_index <= count
      ensure
         Result /= 0 implies item(Result) = c

   first_index_of (c: CHARACTER): INTEGER
      -- Index of first occurrence of c at index 1 or after index 1.

      ensure
         definition: Result = index_of(c,1)

   has (c: CHARACTER): BOOLEAN
      -- True if c is in the STRING.


   has_substring (other: STRING): BOOLEAN
      -- True if Current contains other.

      require
         other_not_void: other /= Void

   occurrences (c: CHARACTER): INTEGER
      -- Number of times character c appears in the string.

      ensure
         Result >= 0

   has_suffix (s: STRING): BOOLEAN
      -- True if suffix of Current is s.

      require
         s /= Void

   has_prefix (p: STRING): BOOLEAN
      -- True if prefix of Current is p.

      require
         p /= Void

feature(s) from STRING
   -- Testing and Conversion:

   is_boolean: BOOLEAN
      -- Does Current represent a BOOLEAN?
      -- Valid BOOLEANs are "True" and "False".


   to_boolean: BOOLEAN
      -- Boolean value
      -- "True" yields True, "False" yields False (what a surprise).

      require
         represents_a_boolean: is_boolean

   is_integer: BOOLEAN
      -- Does 'Current' represent an INTEGER?
      -- Result is true if and only if the following two conditions 
      -- hold: 
      --
      -- 1. In the following BNF grammar, the value of Current can be
      -- produced by "Integer_literal", if leading and trailing
      -- separators are ignored:
      --
      -- Integer_literal = [Sign] Integer
      -- Sign            = "+" | "-"
      -- Integer         = Digit | Digit Integer
      -- Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
      --
      -- 2. The numerical value represented by Current is within the
      -- range that can be represented by an instance of type INTEGER.


   to_integer: INTEGER
      -- Current must look like an INTEGER.

      require
         is_integer

   is_double: BOOLEAN
      -- Can contents be read as a DOUBLE?
      -- Fails for numbers where the base or "10 ^ exponent" are not in
      -- the range Minimum_double ... Maximum_double. Parsing is done
      -- positive. That means if Minimum_double.abs is not equal to
      -- Maximum_double it will not work correctly. Furthermore the
      -- arithmetric package used must support the value 'inf' for a
      -- number greater than Maximum_double.
      -- Result is true if and only if the following two conditions 
      -- hold:
      --
      -- 1. In the following BNF grammar, the value of Current can be
      -- produced by "Real_literal", if leading or trailing separators
      -- are ignored.
      --
      -- Real_literal    = Mantissa [Exponent_part]
      -- Exponent_part   = "E" Exponent
      --                 | "e" Exponent
      -- Exponent        = Integer_literal
      -- Mantissa        = Decimal_literal
      -- Decimal_literal = Integer_literal ["." Integer]
      -- Integer_literal = [Sign] Integer
      -- Sign            = "+" | "-"
      -- Integer         = Digit | Digit Integer
      -- Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
      --
      --
      -- 2. The numerical value represented by Current is within the 
      -- range that can be represented by an instance of type DOUBLE.


   to_double: DOUBLE
      -- Conversion to the corresponding DOUBLE value. The string must
      -- looks like a DOUBLE (or like an INTEGER because fractionnal part
      -- is optional). For an exact definition see 'is_double'.
      -- Note that this conversion might not be exact.

      require
         represents_a_double: is_double

   is_real: BOOLEAN
      -- Can contents be read as a REAL?


   to_real: REAL
      -- Conversion to the corresponding REAL value.
      -- The string must looks like a REAL (or like an
      -- INTEGER because fractionnal part is optional).

      require
         is_integer or is_real

   is_number: BOOLEAN
      -- Can contents be read as a NUMBER?


   to_number: NUMBER
      -- Current must looks like an INTEGER.

      require
         is_number

   is_bit: BOOLEAN
      -- True when the contents is a sequence of bits (i.e., mixed
      -- characters 0 and characters 1).

      ensure
         Result = (count = occurrences('0') + occurrences('1'))

   to_hexadecimal
      -- Convert Current bit sequence into the corresponding
      -- hexadecimal notation.

      require
         is_bit

   binary_to_integer: INTEGER
      -- Assume there is enougth space in the INTEGER to store
      -- the corresponding decimal value.

      require
         is_bit;
         count <= integer_bits

feature(s) from STRING
   -- Modification:

   resize (new_count: INTEGER)
      -- Resize Current. When new_count is greater than
      -- count, new positions are initialized with the
      -- default value of type CHARACTER ('%U').

      require
         new_count >= 0
      ensure
         count = new_count;
         capacity >= old capacity

   clear
      -- Clear out the current STRING.
      -- Note: internal storage memory is neither released nor shrunk.

      ensure
         count = 0

   wipe_out
      -- Clear out the current STRING.
      -- Note: internal storage memory is neither released nor shrunk.

      ensure
         count = 0

   copy (other: like Current)
      -- Copy other onto Current.

      require
         same_dynamic_type(other)
      ensure
         count = other.count;
         is_equal(other)

   fill_with (c: CHARACTER)
      -- Replace every character with c.

      ensure
         occurrences(c) = count

   replace_all (old_character, new_character: like item)
      -- Replace all occurrences of the element old_character by
      -- new_character.

      ensure
         count = old count;
         occurrences(old_character) = 0

   append (s: STRING)
      -- Append a copy of 's' to Current.

      require
         s_not_void: s /= Void

   append_string (s: STRING)
      -- Append a copy of 's' to Current.

      require
         s_not_void: s /= Void

   prepend (other: STRING)
      -- Prepend other to Current.

      require
         other /= Void
      ensure
         Current.is_equal(old other.twin + old Current.twin)

   insert_string (s: STRING; i: INTEGER)
      -- Insert s at index i, shifting characters from index i
      -- to count rightwards.

      require
         string_not_void: s /= Void;
         valid_insertion_index: 1 <= i and i <= count + 1

   replace_substring (s: STRING; start_index, end_index: INTEGER)
      -- Replace the substring from start_index to end_index,
      -- inclusive, with s.

      require
         string_not_void: s /= Void;
         valid_start_index: 1 <= start_index;
         valid_end_index: end_index <= count;
         meaningful_interval: start_index <= end_index + 1

   infix "+" (other: STRING): like Current
      -- Create a new STRING which is the concatenation of
      -- Current and other.

      require
         other_exists: other /= Void
      ensure
         result_count: Result.count = count + other.count

   put (c: CHARACTER; i: INTEGER)
      -- Put c at index i.

      require
         valid_index: valid_index(i)
      ensure
         item(i) = c

   swap (i1, i2: INTEGER)
      require
         valid_index(i1);
         valid_index(i2)
      ensure
         item(i1) = old item(i2);
         item(i2) = old item(i1)

   insert_character (c: CHARACTER; i: INTEGER)
      -- Inserts c at index i, shifting characters from
      -- position 'i' to count rightwards.

      require
         valid_insertion_index: 1 <= i and i <= count + 1
      ensure
         item(i) = c

   shrink (min_index, max_index: INTEGER)
      -- Keep only the slice [min_index .. max_index] or nothing
      -- when the slice is empty.

      require
         1 <= min_index;
         max_index <= count;
         min_index <= max_index + 1
      ensure
         count = max_index - min_index + 1

   remove (i: INTEGER)
      -- Remove character at position i.

      require
         valid_removal_index: valid_index(i)
      ensure
         count = old count - 1

   add_first (c: CHARACTER)
      -- Add c at first position.

      ensure
         count = 1 + old count;
         item(1) = c

   precede (c: CHARACTER)
      -- Add c at first position.

      ensure
         count = 1 + old count;
         item(1) = c

   add_last (c: CHARACTER)
      -- Append c to string.

      ensure
         count = 1 + old count;
         item(count) = c

   append_character (c: CHARACTER)
      -- Append c to string.

      ensure
         count = 1 + old count;
         item(count) = c

   extend (c: CHARACTER)
      -- Append c to string.

      ensure
         count = 1 + old count;
         item(count) = c

   to_lower
      -- Convert all characters to lower case.


   to_upper
      -- Convert all characters to upper case.


   as_lower: like Current
      -- New object with all letters in lower case.


   as_upper: like Current
      -- New object with all letters in upper case.


   keep_head (n: INTEGER)
      -- Remove all characters except for the first n.
      -- Do nothing if n >= count.

      require
         n_non_negative: n >= 0
      ensure
         count = n.min(old count)

   keep_tail (n: INTEGER)
      -- Remove all characters except for the last n.
      -- Do nothing if n >= count.

      require
         n_non_negative: n >= 0
      ensure
         count = n.min(old count)

   remove_head (n: INTEGER)
      -- Remove n first characters. If n >= count, remove all.

      require
         n_non_negative: n >= 0
      ensure
         count = (0).max(old count - n)

   remove_first (n: INTEGER)
      -- Remove n first characters. If n >= count, remove all.

      require
         n_non_negative: n >= 0
      ensure
         count = (0).max(old count - n)

   remove_tail (n: INTEGER)
      -- Remove n last characters. If n >= count, remove all.

      require
         n_non_negative: n >= 0
      ensure
         count = (0).max(old count - n)

   remove_last (n: INTEGER)
      -- Remove n last characters. If n >= count, remove all.

      require
         n_non_negative: n >= 0
      ensure
         count = (0).max(old count - n)

   remove_substring (start_index, end_index: INTEGER)
      -- Remove all characters from strt_index to end_index inclusive.

      require
         valid_start_index: 1 <= start_index;
         valid_end_index: end_index <= count;
         meaningful_interval: start_index <= end_index + 1
      ensure
         count = old count - (end_index - start_index + 1)

   remove_between (start_index, end_index: INTEGER)
      -- Remove all characters from strt_index to end_index inclusive.

      require
         valid_start_index: 1 <= start_index;
         valid_end_index: end_index <= count;
         meaningful_interval: start_index <= end_index + 1
      ensure
         count = old count - (end_index - start_index + 1)

   remove_suffix (s: STRING)
      -- Remove the suffix s of current string.

      require
         has_suffix(s)
      ensure
         (old Current.twin).is_equal(Current + old s.twin)

   remove_prefix (s: STRING)
      -- Remove the prefix s of current string.

      require
         has_prefix(s)
      ensure
         (old Current.twin).is_equal(old s.twin + Current)

   left_adjust
      -- Remove leading blanks.

      ensure
         stripped: is_empty or else item(1) /= ' '

   right_adjust
      -- Remove trailing blanks.

      ensure
         stripped: is_empty or else item(count) /= ' '

feature(s) from STRING
   -- Printing:

   out_in_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.

      ensure
         not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
         append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))

   fill_tagged_out_memory
      -- Append a viewable information in tagged_out_memory in
      -- order to affect the behavior of out, tagged_out, etc.


feature(s) from STRING
   -- Agents based features:

   do_all (action: PROCEDURE[ANY,TUPLE[CHARACTER]])
      -- Apply action to every item of Current.


   for_all (test: PREDICATE[ANY,TUPLE[CHARACTER]]): BOOLEAN
      -- Do all items satisfy test?


   exists (test: PREDICATE[ANY,TUPLE[CHARACTER]]): BOOLEAN
      -- Does at least one item satisfy test?


feature(s) from STRING
   -- Other features:

   first: CHARACTER
      -- Access to the very first character.

      require
         not is_empty
      ensure
         definition: Result = item(1)

   last: CHARACTER
      -- Access to the very last character.

      require
         not is_empty
      ensure
         definition: Result = item(count)

   substring (start_index, end_index: INTEGER): like Current
      -- New string consisting of items [start_index.. end_index].

      require
         valid_start_index: 1 <= start_index;
         valid_end_index: end_index <= count;
         meaningful_interval: start_index <= end_index + 1
      ensure
         substring_count: Result.count = end_index - start_index + 1

   extend_multiple (c: CHARACTER; n: INTEGER)
      -- Extend Current with n times character c.

      require
         n >= 0
      ensure
         count = n + old count

   precede_multiple (c: CHARACTER; n: INTEGER)
      -- Prepend n times character c to Current.

      require
         n >= 0
      ensure
         count = n + old count

   extend_to_count (c: CHARACTER; needed_count: INTEGER)
      -- Extend Current with c until needed_count is reached.
      -- Do nothing if needed_count is already greater or equal
      -- to count.

      require
         needed_count >= 0
      ensure
         count >= needed_count

   precede_to_count (c: CHARACTER; needed_count: INTEGER)
      -- Prepend c to Current until needed_count is reached.
      -- Do nothing if needed_count is already greater or equal
      -- to count.

      require
         needed_count >= 0
      ensure
         count >= needed_count

   reverse
      -- Reverse the string.


   remove_all_occurrences (ch: CHARACTER)
      -- Remove all occurrences of ch.

      ensure
         count = old count - old occurrences(ch)

   substring_index (other: STRING; start_index: INTEGER): INTEGER
      -- Position of first occurrence of other at or after start
      -- 0 if none.

      require
         other_not_void: other /= Void;
         valid_start_index: start_index >= 1 and start_index <= count + 1

   first_substring_index (other: STRING): INTEGER
      -- Position of first occurrence of other at or after 1, 0 if none.

      require
         other_not_void: other /= Void
      ensure
         definition: Result = substring_index(other,1)

feature(s) from STRING
   -- Splitting a STRING:

   split: ARRAY[STRING]
      -- Split the string into an array of words. Uses is_separator of
      -- CHARACTER to find words. Gives Void or a non empty array.

      ensure
         Result /= Void implies not Result.is_empty

   split_in (words: COLLECTION[STRING])
      -- Same jobs as split but result is appended in words.

      require
         words /= Void
      ensure
         words.count >= old words.count

feature(s) from STRING
   -- Other features:

   extend_unless (ch: CHARACTER)
      -- Extend Current (using extend) with ch unless ch is
      -- already the last character.

      ensure
         last = ch;
         count >= old count

   get_new_iterator: ITERATOR[CHARACTER]

feature(s) from STRING
   -- Interfacing with C string:

   to_external: POINTER
      -- Gives C access to the internal storage (may be dangerous).
      -- To be compatible with C, a null character is added at the end
      -- of the internal storage. This extra null character is not
      -- part of the Eiffel STRING.

      ensure
         count = old count;
         Result.is_not_null

   from_external (p: POINTER)
      -- Internal storage is set using p (may be dangerous because
      -- the external C string p is not duplicated). Assume p has a 
      -- null character at the end in order to compute the Eiffel 
      -- count. This extra null character is not part of the Eiffel 
      -- STRING. Also consider from_external_copy to choose the most 
      -- appropriate.

      require
         p.is_not_null
      ensure
         capacity = count + 1;
         p = to_external

   from_external_copy (p: POINTER)
      -- Internal storage is set using a copy of p. Assume p has a 
      -- null character at the end in order to compute the Eiffel 
      -- count. This extra null character is not part of the Eiffel 
      -- STRING. Also consider from_external to choose the most 
      -- appropriate.

      require
         p.is_not_null

   from_c (p: POINTER)
      -- Internal storage is set using a copy of p. Assume p has a 
      -- null character at the end in order to compute the Eiffel 
      -- count. This extra null character is not part of the Eiffel 
      -- STRING. Also consider from_external to choose the most 
      -- appropriate.

      require
         p.is_not_null

feature(s) from STRING
   -- Other features here for ELKS compatibility:

   make_from_string (model: STRING)
      -- (Here for ELKS compatibility.)
      -- Initialize from the characters of model.
      -- Useful in proper descendants of STRING.

      require
         model /= Void
      ensure
         count = model.count

   same_string (other: STRING): BOOLEAN
      -- (Here for ELKS compatibility.)
      -- Do Current and other have the same character sequence?
      -- Useful in proper descendants of STRING.

      require
         other_not_void: other /= Void

   string: STRING
      -- (Here for ELKS compatibility.)
      -- New STRING having the same character sequence as Current.
      -- Useful in proper descendants of STRING.



invariant
   0 <= count;
   count <= capacity;
   capacity > 0 implies storage.is_not_null;

end of STRING