class interface P_SHRINK_STRING creation make (a_string: STRING) -- Setup virtual string. require not_void: a_string /= Void feature(s) from P_SHRINK_STRING -- Conversion to_string: STRING -- String (non mutable, may be original) corresponding to the -- correspondingly shrinked string. feature(s) from P_SHRINK_STRING -- General is_equal (s_string: like Current): BOOLEAN -- Equality. require other_not_void: s_string /= Void ensure consistent: standard_is_equal(s_string) implies Result; symmetric: Result implies s_string.is_equal(Current) is_start (other: P_SHRINK_STRING): BOOLEAN -- Is current start of other? require not_void: other /= Void is_first_one_of (some_chars: STRING): BOOLEAN -- Is first character a character from some_chars? require has_first: count > 0; chars_not_void: some_chars /= Void duplicate: P_SHRINK_STRING -- New shrink string equal to this one. feature(s) from P_SHRINK_STRING -- Operation(s) remove_first -- Remove a character at start require has_char: count > 0 ensure done: count = old count - 1 remove_start (n: INTEGER) -- Remove 'n' characters at start. require has_chars: count >= n ensure done: count = old count - n remove_last -- Remove character at end. require has_char: count > 0 ensure done: count = old count - 1 remove_end (n: INTEGER) -- Remove 'n' characters at end. require has_chars: count >= n ensure done: count = old count - n skip_character (a_char: CHARACTER) -- Remove all occurences of character at start of virtual string. ensure skipped: is_empty or else first /= a_char; shrinked: count <= old count skip_characters (some_chars: STRING) -- Remove all occurences of characters in 'some_chars' at start of virtual string. require not_void: some_chars /= Void; not_empty: not some_chars.empty ensure shrinked: count <= old count count: INTEGER -- Number of characters in virtual string. ensure positive: count >= 0 is_empty: BOOLEAN -- Empty virtual string? item (an_index: INTEGER): CHARACTER -- Characters in virtual string. require low_index: an_index >= 1; up_index: an_index <= count first: CHARACTER -- First character of string. require has_char: count > 0 last: CHARACTER -- Last character of string. require has_char: count > 0 invariant string_is: string /= Void; dead_max: dead_start + dead_end <= string.count; end of P_SHRINK_STRING