class interface STRING
   -- 
   --  Resizable character STRINGs. 
   -- 

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
         other_not_void: other /= Void
      ensure
         count = other.count;
         is_equal: is_equal(other)

   blank (nr_blanks: INTEGER)
      --  Initialize string with nr_blanks blanks.

      require
         nr_blanks >= 0
      ensure
         count = nr_blanks;
         occurrences_of(' ') = 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.


   make_from_string (s: STRING)
      --  Initialize from the characters of s.
      --  (Useful in proper descendants of class STRING, to 
      --  initialize a string-like object from a manifest string.)

      require
         s /= Void
      ensure
         count = s.count

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

      ensure
         good_hash_value: Result >= 0

feature(s) from COMPARABLE
   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.


   capacity: INTEGER
      --  Capacity of the storage.


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

   blank (nr_blanks: INTEGER)
      --  Initialize string with nr_blanks blanks.

      require
         nr_blanks >= 0
      ensure
         count = nr_blanks;
         occurrences_of(' ') = count

feature(s) from STRING
   --  Testing :

   empty: BOOLEAN
      --  Has string length 0?


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

      require
         valid_index(index)

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

      require
         valid_index(index)

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

      ensure
         Result = (1 <= index and then index <= count)

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

      require
         other /= Void

   is_equal (other: like Current): BOOLEAN
      --  Has Current the same text as other ?

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

   index_of (ch: CHARACTER): INTEGER
      --  Gives the index of the first occurrence ch or 
      --  count + 1 if none.

      ensure
         Result /= count + 1 implies item(Result) = ch

   index_of_string (other: STRING): INTEGER
      --  Position of the first occurrence of other
      --  or count + 1 if none.

      require
         not other.empty

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


   has_string (other: STRING): BOOLEAN
      --  True if other is in the STRING.


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

      ensure
         Result >= 0

   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

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

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

   is_integer: BOOLEAN
      --  Can contents be read as an INTEGER ?


   is_real: BOOLEAN
      --  Contents can be read as a REAL.


   is_double: BOOLEAN
      --  Contents can be read as a DOUBLE.


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

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

feature(s) from STRING
   --  Modification :

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

      ensure
         count = 0

feature(s) from STRING
   --  Modification :

   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
         other_not_void: other /= Void
      ensure
         count = other.count;
         is_equal: is_equal(other)

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

      ensure
         occurrences_of(c) = count

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

      ensure
         occurrences_of(c) = count

   fill_blank
      --  Fill entire string with blanks

      ensure
         occurrences_of(' ') = count

   append (other: STRING)
      --  Append other to Current.

      require
         other /= Void

   append_string (other: STRING)
      --  Append other to Current.

      require
         other /= Void

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

      require
         other /= Void
      ensure
         count = other.count + old count

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

      require
         other /= Void
      ensure
         Result.count = count + other.count

   put (ch: CHARACTER; index: INTEGER)
      --  Put ch at position index.

      require
         valid_index(index)
      ensure
         item(index) = ch

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

   insert (ch: CHARACTER; index: INTEGER)
      --  Insert ch after position index.

      require
         0 <= index and index <= count
      ensure
         item(index + 1) = ch

   shrink (low, up: INTEGER)
      --  Keep only the slice low .. up or nothing
      --  when the slice is empty.

      require
         1 <= low;
         low <= count;
         1 <= up;
         up <= count
      ensure
         up > low implies count = up - low + 1

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

      require
         valid_index(index)
      ensure
         count = old count - 1

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

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

   add_last (ch: CHARACTER)
      --  Append ch to string

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

   extend (ch: CHARACTER)
      --  Append ch to string

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

   append_character (ch: CHARACTER)
      --  Append ch to string

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

   precede (ch: CHARACTER)
      --  Prepend ch to string

      ensure
         item(1) = ch

   to_lower
      --  Convert all characters to lower case.


   to_upper
      --  Convert all characters to upper case.


   remove_first (nb: INTEGER)
      --  Remove nb first characters.

      require
         nb >= 0;
         count >= nb
      ensure
         count = old count - nb

   remove_last (nb: INTEGER)
      --  Remove nb last characters.

      require
         0 <= nb;
         nb <= count
      ensure
         count = old count - nb

   remove_between (low, up: INTEGER)
      --  Remove character between positions low and up.

      require
         valid_index(low);
         valid_index(up);
         low <= up
      ensure
         count = old count - up - low + 1

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

      require
         has_suffix(s)
      ensure
         old count = count + s.count

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

      require
         has_prefix(s)
      ensure
         old count = count + s.count

   left_adjust
      --  Remove leading blanks.

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

   right_adjust
      --  Remove trailing blanks.

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

feature(s) from STRING
   --  Features which don't modify the string

   first: CHARACTER
      require
         not empty

   last: CHARACTER
      require
         not empty

feature(s) from STRING
   --  Conversion :

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

      require
         is_integer

   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

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

      require
         is_integer or is_real

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

      require
         is_bit;
         count <= Integer_bits

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

      require
         is_bit

feature(s) from STRING
   --  Printing :

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


   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
   --  Other features :

   substring (low, up: INTEGER): like Current
      --  Create a new string initialized with range low.. up.  

      require
         1 <= low;
         low <= up;
         up <= count

   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_of(ch)

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

      require
         start_large_enough: start >= 1;
         start_small_enough: start <= count;
         string_exist: other /= Void

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.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 feature :

   set_last (ch: CHARACTER)
      ensure
         last = ch

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.


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

   make_from_string (s: STRING)
      --  Initialize from the characters of s.
      --  (Useful in proper descendants of class STRING, to 
      --  initialize a string-like object from a manifest string.)

      require
         s /= Void
      ensure
         count = s.count

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

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

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

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

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

end of STRING