Class STRING

Draft Proposal 15 September 1999
compiled by Dominique Colnet and Olivier Zendra

indexing

description: "Resizable sequences of characters, accessible through %
    %integer indices in a contiguous range. If not empty, first element%
    %is at index 1."

class interface

STRING

creation

make (n: INTEGER)
        -- Allocate space for at least n characters.
    require
        non_negative_size: n >= 0
    ensure
        empty_string: count = 0
        correctly_allocated_size: capacity >= n

make_from_external (ptr: POINTER)
        -- Set Current with a copy of the content of ptr.
        -- Assume ptr is a null-terminated memory area containing
        -- only characters.
        -- The extra null character is not part of the Eiffel string
    require
        ptr_exists: ptr /= default_pointer

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
        string_exists: s /= Void
    ensure
        count_set: count = s.count

feature -- Initialization

make (n: INTEGER)
        -- Allocate space for at least n characters.
    require
        non_negative_size: n >= 0
    ensure
        empty_string: count = 0
        correctly_allocated_size: capacity >= n

make_from_external (ptr: POINTER)
        -- Set Current with a copy of the content of ptr.
        -- Assume ptr is a null-terminated memory area containing
        -- only characters.
        -- The extra null character is not part of the Eiffel string
    require
        ptr_exists: ptr /= default_pointer

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
        string_exists: s /= Void
    ensure
        count_set: count = s.count

feature -- Access

first: CHARACTER
        -- First character of Current.
    require
        not_empty_string: not is_empty
    ensure
        good_result: Result = item (1)

has (c: CHARACTER): BOOLEAN
        -- Does Current contain c ? 
    ensure
        definition: Result = (index_of(c) /= 0);

hash_code: INTEGER
        -- Hash code value
        -- (From HASHABLE.)
    ensure
        good_hash_value: Result >= 0

index_from (c: CHARACTER; start_index: INTEGER): INTEGER
        -- Index of first occurrence of c at or after start_index; 
        -- 0 if none.
    require
        valid_start_index: valid_index (start_index)
    ensure
        non_negative_result: Result >= 0;
        valid_result: Result > 0 implies valid_index (Result)
        result_after_start_index: Result > 0 implies Result >= start_index;
        at_this_index: Result > 0 implies item (Result) = c;
        -- none_before: For every i in start_index..Result-1, item (i) /= c
        -- zero_iff_absent:
        --     (Result = 0) = For every i in start_index..count, item (i) /= c

index_of (c: CHARACTER): INTEGER
        -- Index of first occurrence of c; 
        -- 0 if none.
    ensure
        empty_definition: empty implies Result = 0;
        non_empty_definition: not empty implies Result = index_from (c, 1);

infix "@", item (i: INTEGER): CHARACTER
        -- Character at index i
    require
        good_key: valid_index (i)

last: CHARACTER
        -- Last character of Current.
    require
        not_empty_string: not is_empty
    ensure
        good_result: Result = item (count)

reverse_index_from (c: CHARACTER; last_index: INTEGER): INTEGER
        -- Index of first occurrence of c at or before last_index; 
        -- 0 if none.
    require
        valid_last_index: valid_index (last_index)
    ensure
        non_negative_result: Result >= 0;
        valid_result: Result > 0 implies valid_index(Result)
        result_before_last_index: Result <= last_index;
        at_this_index: Result > 0 implies item (Result) = c;
        -- none_before: Result > 0 implies For every i in Result+1..last_index, item (i) /= c
        -- zero_iff_absent:
        --     (Result = 0) = For every i in 1..last_index, item (i) /= c

reverse_index_of (c: CHARACTER): INTEGER
        -- Index of last occurrence of c; 
        -- 0 if none.
    ensure
        empty_definition: empty implies Result = 0;
        non_empty_definition: empty implies Result = reverse_index_from (c, count);

reverse_string_index_from (other: STRING; last_index: INTEGER): INTEGER
        -- Index of first occurrence of other at or before last_index;
        -- 0 if none.
    require
        other_not_empty: not other.empty;
        valid_last_index: valid_index (last_index)
    ensure
        non_negative_result: Result >= 0;
        valid_result: Result > 0 implies valid_index (Result)
        result_before_last_index: Result > 0 implies Result <= last_index;
        at_this_index: Result > 0 implies other.is_equal (substring (Result, Result - 1 + other.count));
        -- none_before: Result > 0 implies
        --     For every i in Result+1..last_index, not other.is_equal (substring (i, i - 1 + other.count))
        -- zero_iff_absent:
        --     (Result = 0) = For every i in 1..last_index, not other.is_equal (substring (i, i - 1 + other.count))

reverse_string_index_of (other: STRING): INTEGER
        -- Index of last occurrence of other; 
        -- 0 if none.
    require
        other_not_empty: not other.empty
    ensure
        empty_definition: empty implies Result = 0;
        non_empty_definition: not empty implies Result = reverse_string_index_from (other, count);

string_index_from (other: STRING; start_index: INTEGER): INTEGER
        -- Index of first occurrence of other at or after start; 
        -- 0 if none.
    require
        other_not_empty: not other.empty;
        valid_start_index: valid_index (start_index)
    ensure
        non_negative_result: Result >= 0;
        valid_result: Result > 0 implies valid_index (Result)
        result_after_start_index: Result > 0 implies Result >= start_index;
        at_this_index: Result > 0 implies other.is_equal (substring (Result, Result - 1+ other.count));
        -- none_before:
        --     For every i in start_index..Result-1, not other.is_equal (substring (i, i - 1 + other.count))
        -- zero_iff_absent:
        --     (Result = 0) = For every i in start_index..count, not other.is_equal (substring (i, i - 1 + other.count))

string_index_of (other: STRING): INTEGER
        -- Index of first occurrence of other; 
        -- 0 if none.
    require
        other_not_empty: not other.empty
    ensure
        empty_definition: empty implies Result = 0;
        non_empty_definition: not empty implies Result = reverse_string_index_from (other, 1);

feature -- Measurement

count: INTEGER
        -- Current number of characters making up the string

capacity: INTEGER
        -- Number of characters that Current can currently contain in the internal storage area.
        -- Automatically updated when resizing is needed. Useful for fine tuning.

occurrences (c: CHARACTER): INTEGER
        -- Number of times c appears in the string
    ensure
        non_negative_occurrences: Result >= 0

feature -- Comparison

is_equal (other: like Current): BOOLEAN
        -- Is string made of same character sequence as other?
        -- (Redefined from GENERAL.)
    require
        other_exists: other /= Void

infix "<" (other: like Current): BOOLEAN
        -- Is string lexicographically lower than other?
        -- (False if other is void)
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        asymmetric: Result implies not (other < Current)

infix "<=" (other: like Current): BOOLEAN
        -- Is current object less than or equal to other?
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        definition: Result = (Current < other) or is_equal (other);

infix ">=" (other: like Current): BOOLEAN
        -- Is current object greater than or equal to other?
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        definition: Result = (other <= Current)

infix ">" (other: like Current): BOOLEAN
        -- Is current object greater than other?
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        definition: Result = (other < Current)

max (other: like Current): like Current)
        -- The greater of current object and other
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        current_if_not_smaller: (Current >= other) implies (Result = Current)
        other_if_smaller: (Current < other) implies (Result = other)

min (other: like Current): like Current)
        -- The smaller of current object and other
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        current_if_not_greater: (Current <= other) implies (Result = Current)
        other_if_greater: (Current > other) implies (Result = other)

same_as (other: STRING): BOOLEAN
        -- Is string made of same character sequence as other?
        -- Case insensitive comparison.
    require
        other_exists: other /= Void

three_way_comparison (other: like Current): INTEGER
        -- If current object equal to other, 0; if smaller,
        -- -1; if greater, 1.
        -- (From COMPARABLE.)
    require
        other_exists: other /= Void
    ensure
        equal_zero: (Result = 0) = is_equal (other);
        smaller: (Result = -1) = Current < other;
        greater_positive: (Result = 1) = Current > other

feature -- Status report

is_empty: BOOLEAN
        -- Is string empty?
    ensure
        definition: Result = (count = 0)

valid_index (index: INTEGER): BOOLEAN
        -- Is i within the bounds of the string?
    ensure
        definition: Result = (1 <= index and index <= count)

is_boolean: BOOLEAN
        -- Is Current representing a boolean ("true" or "false" with no
        -- case consideration)?

is_double: BOOLEAN
        -- Can Current be read as a DOUBLE?

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

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

feature -- Element change

add, insert (c: CHARACTER; i: INTEGER)
        -- Insert c at index i, shifting characters between ranks i and count rightwards.
    require
        valid_insertion_index: 1 <= i and i <= count + 1
    ensure
         inserted: item (i) = c
         one_more_character: count = old count + 1

add_first, precede (c: CHARACTER)
        -- Prepend c at beginning.
    ensure
        inserted: first = c
        one_more_character: count = old count + 1

add_last, append_character, extend (c: CHARACTER)
        -- Append c at end.
    ensure
        inserted: last = c
        one_more_character: count = old count + 1

append, append_string (s: STRING)
        -- Append a copy of s at end.
    require
        other_exists: s /= Void
    ensure
        new_count: count = old count + old s.count
        -- appended: For every i in 1.. old s.count,
        --     item (old count + i) = s.item (i)

append_boolean (b: BOOLEAN)
        -- Append the string representation of b at end.
    ensure
        boolean_inserted: reverse_index_of (b.out) = count - b.out.count
        new_count: count = old count + b.out.count + 1

append_double (d: DOUBLE)
        -- Append the string representation of d at end.
    ensure
        double_inserted: reverse_index_of (d.out) = count - d.out.count
        new_count: count = old count + d.out.count + 1

append_integer (i: INTEGER)
        -- Append the string representation of i at end.
    ensure
        integer_inserted: reverse_index_of (i.out) = count - i.out.count
        new_count: count = old count + i.out.count + 1

append_real (r: REAL)
        -- Append the string representation of r at end.
    ensure
        real_inserted: reverse_index_of (r.out) = count - r.out.count
        new_count: count = old count + r.out.count + 1

fill (c: CHARACTER)
        -- Replace every character with c.
    ensure
        same_count: old count = count
        filled: occurrences(c) = count

head (n: INTEGER)
        -- Remove all characters except for the first n; 
        -- do nothing if n >= count.
    require
        non_negative_argument: n >= 0
    ensure
        new_count: count = n.min (old count)
        -- first_kept: For every i in 1..n, item (i) = old item (i)

insert_string (s: like Current; i: INTEGER)
        -- Insert s at index i, shifting characters between ranks i and count rightwards.
    require
        string_exists: s /= Void; 
        valid_insertion_index: 1 <= i and i <= count + 1
    ensure
        new_count: count = old count + old s.count
        inserted: s.is_equal (substring (i, i - 1 + old s.count))

left_adjust
        -- Remove leading white space.
    ensure
        shorter: count <= old count
        first_not_white_space: not is_empty implies ("%T%R%N ").index_of (first) = 0

put (c: CHARACTER; i: INTEGER)
        -- Replace character at index i by c.
    require
        good_key: valid_index (i)
    ensure
        insertion_done: item (i) = c

right_adjust
        -- Remove trailing white space.
    ensure
        shorter: count <= old count
        last_not_white_space: not is_empty implies ("%T%R%N ").index_of (last) = 0

subcopy (other: like Current; start_pos, end_pos, from_index: INTEGER) is
        -- Copy characters of other within bounds start_pos and
        -- end_pos to current string starting at index from_index.
    require
        other_not_void: other /= Void;
        valid_start_pos: other.valid_index (start_pos)
        valid_end_pos: other.valid_index (end_pos)
        valid_bounds: start_pos <= end_pos
        valid_from_index: valid_index (from_index)
        enough_space: valid_index (from_index + end_pos - start_pos)
    ensure
        same_count: old count = count
        copied: substring (from_index, from_index + end_pos - start_pos).is_equal
                 (other.substring (start_pos, end_pos))

tail (n: INTEGER)
        -- Remove all characters except for the last n; 
        -- do nothing if n >= count.
    require
        non_negative_argument: n >= 0
    ensure
        new_count: count = n.min (old count)

feature -- Removal

remove (i: INTEGER)
         -- Remove i-th character, shifting characters between ranks i + 1 and count leftwards.
    require
        valid_removal_index: valid_index (i)
    ensure
        new_count: count = old count - 1

wipe_out
        -- Remove all characters.
    ensure
        empty_string: is_empty
        same_capacity: capacity = old capacity
        same_lower: lower = old lower

feature -- Conversion

to_boolean: BOOLEAN
        -- Boolean value; 
        -- "true" yields true, "false" yields false
        -- (case-insensitive)
    require
        is_boolean: is_boolean

to_double: DOUBLE
        -- Double value; for example, when applied to "123.0",
        -- will yield 123.0 (double)
    require
        is_double: is_integer or is_real or is_double

to_external: POINTER
        -- Address of the storage area containing the actual sequence of characters,
        -- to be passed to some external (non-Eiffel) routine.
        -- Keep in mind that this storage area is subject to garbage collection.

to_integer: INTEGER
        -- Integer value; 
        -- for example, when applied to "123", will yield 123
    require
        is_integer: is_integer

to_lower
        -- Convert to lower case.

to_real: REAL
        -- Real value; 
        -- for example, when applied to "123.0", will yield 123.0
    require
        is_real: is_integer or is_real

to_upper
        -- Convert to upper case.

feature -- Duplication

copy (other: like Current)
        -- Reinitialize by copying the characters of other.
        -- (From GENERAL.)
    ensure
        new_result_count: count = other.count
        -- same_characters: For every i in 1..count,
        --     item (i) = other.item (i)

infix "+" (other: STRING): like Current
        -- Create a new object which is the concatenation of Current and other.
    require
        other_exists: other /= Void
    ensure
        result_count: Result.count = count + other.count

substring (start_index, end_index: INTEGER): like Current
        -- Create a substring containing all characters from start_index
        -- to end_pos included.
    require
        valid_start_index: valid_index (start_index) 
        valid_end_index: valid_index (end_index)
        meaningful_interval: start_index <= end_index
    ensure
        new_result_count: Result.count = end_index - start_index + 1
        -- original_characters: For every i in 1..end_index - start_index + 1,
        --     Result.item (i) = item (start_index + i -1)

feature -- Output

out: STRING
        -- Printable representation
        -- (From GENERAL.)
    ensure
        result_not_void: Result /= Void
        duplicated_result: Result /= Current and Result.is_equal (Current)

feature -- Optimization

adjust_capacity (n: INTEGER)
        -- Rearrange string so that it can accommodate
        -- at least n characters.
        -- Do not lose any previously entered character.
    require
        no_item_lost: n >= count
    ensure
        enough_capacity: capacity >= n

invariant

non_negative_count: count >= 0
capacity_big_enough: capacity >= count

end