class BACKTRACKING_REGULAR_EXPRESSION

Features exported to ABSTRACT_BACKTRACKING_SEQUENCE

matcher for regular expressions

Direct parents

conformant parents

BACKTRACKING, REGULAR_EXPRESSION

non-conformant parents

REGULAR_EXPRESSION_STRING_SCANNER

Summary

creation features

exported features

common

creation

Common client features

Control of the exploration

Specific to sequences

the pools

matching capabilities

substitution capabilities

Error informations

make

basic

error managment

scanning

Details

make

Creation.

set_scanned_string (string: STRING)

Set 'scanned_string' to 'string'.

ensure

  • match_reset: not last_match_succeeded
  • definition: scanned_string = string
  • at_the_begin: position = scanned_string.lower

last_match_succeeded: BOOLEAN

True if the last match (match_first or match_next) operation was a success.

group_count: INTEGER

The count of groups

invalidate_last_match

Used to prevent 2 substitutions without intermediate matching.

require

  • True
  • last_match_succeeded

ensure

  • not last_match_succeeded
  • not can_substitute

basic_match_first

Starts to match and try to find the first substring of 'scanned_string' that matches the regular expression.

require

  • scanned_string_not_void: scanned_string /= Void

ensure

  • scanned_string_remains: scanned_string = old scanned_string

basic_match_next

Continues to match and try to find the next substring of 'scanned_string' that matches the regular expression.

require

  • scanned_string_not_void: scanned_string /= Void
  • has_result: last_match_succeeded
  • at_good_position: position = last_match_last_index + 1

ensure

  • scanned_string_remains: scanned_string = old scanned_string

match_from (text: STRING, first_index: INTEGER): BOOLEAN

Returns True if Current regular_expression can match the text starting from first_index.

See also match, last_match_succeeded, last_match_first_index.

require

  • text /= Void
  • first_index.in_range(1, text.count + 1)

ensure

  • Result = last_match_succeeded
  • Result implies last_match_first_index >= first_index
  • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
  • Result implies last_match_first_index <= last_match_last_index + 1

matches_only_current_position: BOOLEAN

Does the matching occur only from current position? If that falg is True then:

  * if match succeeds then position is advanced
  * if match fails the position remains
see also 'goto_position'

set_matches_only_current_position (value: BOOLEAN)

Sets 'matches_only_current_position' to 'value'.

ensure

  • definition: matches_only_current_position = value

make

Creation.

set_pattern (pattern: BACKTRACKING_REGULAR_EXPRESSION_PATTERN)

Set the matched pattern.

require

  • valid_pattern: pattern.is_valid

ensure

  • group_count_set: group_count = pattern.group_count
  • match_reset: not last_match_succeeded

set_current_node (node: BACKTRACKING_NODE)

Set the next node of the BACKTRACKING_NODE graph to be evaluated.

ensure

    push_and (node: BACKTRACKING_NODE)

    Pushes 'node' in front of the continuation path.

    require

    • node_not_void: node /= Void

    push_and_list (list: BACKTRACKING_NODE_AND_LIST)

    Pushes 'list' in front of the continuation path.

    require

    • list_not_void: list /= Void

    push_or (node: BACKTRACKING_NODE)

    Pushes 'node' in front of the possible alternatives.

    require

    • node_not_void: node /= Void

    push_or_list (list: BACKTRACKING_NODE_OR_LIST)

    Pushes 'list' in front of the possible alternatives.

    require

    • list_not_void: list /= Void

    search_first

    Resets all and searchs the first solution. The current state must be set. It is the first state, the root of the search. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False, it means that there is no solution at all. Conversly, if search_is_success=True, then the first solution is found and 'search_next' can be called to get the next solution if it exists.

    ensure

    • success_or_off: search_is_success and not is_off or is_off and not search_is_success

    search_next

    Searchs the next solution. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False at the end, it means that there is no more solution. Conversly, if search_is_success=True, then a solution is found and 'search_next' can be called again to get the next solution.

    require

    • last_search_was_a_success: search_is_success

    ensure

    • success_or_off: search_is_success and not is_off or is_off and not search_is_success

    search_is_success: BOOLEAN

    True when search is successfull

    is_off: BOOLEAN

    True when search is finished

    ensure

    • definition: Result = not search_is_success

    clear

    Clears the current state to nothing.

    ensure

    • cleared: is_cleared
    • no_solution: is_off

    is_cleared: BOOLEAN

    True if no partial data remain in the current state

    ensure

    • no_solution_when_cleared: Result implies is_off

    push_sequence (sequence: ABSTRACT_BACKTRACKING_SEQUENCE)

    Pushs the 'sequence' in front of the continuation path.

    require

    • sequence_not_void: sequence /= Void

    ensure

    • is_on_top: top_sequence = sequence
    • is_first_continuation: current_continuation = sequence

    push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

    Pushs the 'alternative' before the continuation path.

    require

    • alternative_not_void: alternative /= Void

    ensure

      continue

      Continues the exploration of the current path.

      backtrack

      Stops the exploration of the current path and tries to explore the next alternative path.

      push_cut_point

      Inserts a cut point into the continuation path. The inserted cut point records the current to of the alternatives.

      cut

      Removes the alternatives until the one recorded by the next cut point in the continuation path.

      cut_all

      Cuts all alternatives.

      top_sequence: ABSTRACT_BACKTRACKING_SEQUENCE

      Stack of sequences represented by its top (can be Void)

      current_continuation: ABSTRACT_BACKTRACKING_SEQUENCE

      The current continuation path

      pop_sequence

      Removes the current sequence and replace it by the next sequence in the continuation path.

      require

      • top_sequence /= Void
      • current_continuation /= Void

      pool_of_cut_points: ABSTRACT_BACKTRACKING_POOL_OF_CUT_POINT

      Bank of cut points

      pool_of_sequence: BACKTRACKING_POOL_OF_SEQUENCE
      pool_of_sequence_list: BACKTRACKING_POOL_OF_SEQUENCE_LIST
      pool_of_alternative: BACKTRACKING_POOL_OF_ALTERNATIVE
      pool_of_alternative_list: BACKTRACKING_POOL_OF_ALTERNATIVE_LIST
      match (text: STRING): BOOLEAN

      Returns True if Current regular_expression can match the text.

      See also match_next, match_from, last_match_succeeded, last_match_first_index.

      require

      • text /= Void

      ensure

      • Result = last_match_succeeded
      • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
      • Result implies last_match_first_index <= last_match_last_index + 1

      match_next (text: STRING): BOOLEAN

      Returns True if Current regular_expression can match the same text one more time. Must be called after a successful match or math_from or match_next using the same text.

      See also match, match_from, last_match_succeeded.

      require

      • text /= Void
      • last_match_succeeded

      ensure

      • Result = last_match_succeeded
      • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
      • Result implies last_match_first_index <= last_match_last_index + 1

      last_match_first_index: INTEGER

      The starting position in the text where starts the sub-string who is matching the whole pattern.

      See also match, match_from.

      require

      • last_match_succeeded

      ensure

      • Result > 0

      last_match_last_index: INTEGER

      The last position in the text where starts the sub-string who is matching the whole pattern.

      See also match, match_from.

      require

      • last_match_succeeded

      ensure

      • Result + 1 >= last_match_first_index

      last_match_count: INTEGER

      Length of the string matching the whole pattern.

      See also last_match_first_index, last_match_last_index, match, match_from.

      require

      • last_match_succeeded

      ensure

      • Result >= 0
      • definition: Result = last_match_last_index - last_match_first_index + 1

      ith_group_matched (i: INTEGER): BOOLEAN

      Did the ith group matched during last match?

      See also group_count, ith_group_first_index.

      require

      • i.in_range(0, group_count)
      • last_match_succeeded

      ith_group_first_index (i: INTEGER): INTEGER

      First index in the last matching text of the ith group of Current.

      See also group_count.

      require

      • i.in_range(0, group_count)
      • last_match_succeeded
      • ith_group_matched(i)

      ensure

        ith_group_last_index (i: INTEGER): INTEGER

        Last index in the last matching text of the ith group of Current.

        See also ith_group_first_index, group_count.

        require

        • i.in_range(0, group_count)
        • last_match_succeeded
        • ith_group_matched(i)

        ensure

          ith_group_count (i: INTEGER): INTEGER

          Length of the ith group of Current in the last matching.

          See also ith_group_first_index, append_ith_group, group_count.

          require

          • i.in_range(0, group_count)
          • last_match_succeeded
          • ith_group_matched(i)

          ensure

          • Result >= 0
          • Result = ith_group_last_index(i) - ith_group_first_index(i) + 1

          append_heading_text (text: STRING, buffer: STRING)

          Append in buffer the text before the matching area. text is the same as used in last matching.

          See also append_pattern_text, append_tailing_text, append_ith_group.

          require

          • text /= Void
          • buffer /= Void
          • last_match_succeeded

          ensure

          • buffer.count = old buffer.count + last_match_first_index - 1

          append_pattern_text (text: STRING, buffer: STRING)

          Append in buffer the text matching the pattern. text is the same as used in last matching.

          See also append_heading_text, append_tailing_text, append_ith_group.

          require

          • text /= Void
          • buffer /= Void
          • last_match_succeeded

          ensure

          • buffer.count = old buffer.count + last_match_count

          append_tailing_text (text: STRING, buffer: STRING)

          Append in buffer the text after the matching area. text is the same as used in last matching.

          See also append_heading_text, append_pattern_text, append_ith_group.

          require

          • text /= Void
          • buffer /= Void
          • last_match_succeeded

          ensure

          • buffer.count = old buffer.count + text.count - last_match_last_index

          append_ith_group (text: STRING, buffer: STRING, i: INTEGER)

          Append in buffer the text of the ith group. text is the same as used in last matching.

          See also append_pattern_text, group_count.

          require

          • text /= Void
          • buffer /= Void
          • last_match_succeeded
          • i.in_range(0, group_count)
          • ith_group_matched(i)

          ensure

          • buffer.count = old buffer.count + ith_group_count(i)

          prepare_substitution (p: STRING)

          Set pattern p for substitution. If pattern p is not compatible with the Current regular expression, the pattern_error_message is updated as well as pattern_error_position.

          See also substitute_in, substitute_for, substitute_all_in, substitute_all_for.

          require

          • p /= Void

          ensure

          • substitution_pattern_ready xor pattern_error_message /= Void

          last_substitution: STRING

          You need to copy this STRING if you want to keep it.

          substitute_for (text: STRING)

          This call has to be precedeed by a sucessful matching on the same text. Then the substitution is made on the matching part. The result is in last_substitution.

          See also prepare_substitution, last_substitution, substitute_in.

          require

          • can_substitute
          • text /= Void

          ensure

          • last_substitution /= Void
          • substitution_pattern_ready
          • only_one_substitution_per_match: not can_substitute

          substitute_in (text: STRING)

          This call has to be precedeed by a sucessful matching on the same text. Then the substitution is made in text on the matching part (text is modified).

          See also prepare_substitution, substitute_for.

          require

          • can_substitute
          • text /= Void

          ensure

          • substitution_pattern_ready
          • only_one_substitution_per_match: not can_substitute

          substitute_all_for (text: STRING)

          Every matching part is substituted. No preliminary matching is required. The result is in last_substitution.

          See also prepare_substitution, last_substitution, substitute_all_in.

          require

          • substitution_pattern_ready
          • text /= Void

          ensure

          • last_substitution /= Void
          • substitution_pattern_ready

          substitute_all_in (text: STRING)

          Every matching part is substituted. No preliminary matching is required. text is modified according to the substitutions is any.

          See also prepare_substitution, last_substitution, substitute_all_for.

          require

          • substitution_pattern_ready
          • text /= Void

          ensure

          • substitution_pattern_ready

          can_substitute: BOOLEAN

          Substitution is only allowed when some valid substitution pattern has been registered and after a sucessful pattern matching.

          See also substitute_in, substitute_for.

          ensure

          • definition: Result = (substitution_pattern_ready and last_match_succeeded)

          substitution_pattern_ready: BOOLEAN

          True if some valid substitution pattern has been registered.

          pattern_error_message: STRING

          Error message for the substitution pattern.

          See also prepare_substitution.

          pattern_error_position: INTEGER

          Error position in the substitution pattern.

          See also prepare_substitution.

          make

          Initialise the attributes.

          scanned_string: STRING

          The expression being currently build.

          set_scanned_string (string: STRING)

          Set the 'scanned_string' with 'string'.

          ensure

          • has_no_error: not has_error
          • definition: scanned_string = string
          • at_the_begin: position = scanned_string.lower

          has_error: BOOLEAN

          True when an error was encountered

          clear_error

          Remove the error flag

          ensure

          • has_no_error: not has_error

          last_error: STRING

          Returns a string recorded for the error.

          require

          • has_error: has_error

          ensure

          • not_void: Result /= Void

          set_error (message: STRING)

          Set has_error and last_error. The explaining error string 'last_error' is created as follow: "Error at position 'position': 'message'.".

          require

          • message_not_void: message /= Void
          • has_no_error: not has_error

          ensure

          • has_error: has_error

          position: INTEGER

          The scanned position. It is the position of 'last_character'.

          last_character: CHARACTER

          The scanned character. The last character readden from 'scanned_string'.

          valid_last_character: BOOLEAN

          True when 'last_character' is valid. Is like 'scanned_string.valid_index(position)'

          valid_previous_character: BOOLEAN

          True if the position-1 is a valid position.

          require

          • scanned_string /= Void

          ensure

          • definition: Result = scanned_string.valid_index(position - 1)

          previous_character: CHARACTER

          The character at position-1.

          require

          • valid_previous_character

          ensure

          • definition: Result = scanned_string.item(position - 1)

          valid_next_character: BOOLEAN

          True if the position+1 is a valid position.

          require

          • scanned_string /= Void

          ensure

          • definition: Result = scanned_string.valid_index(position + 1)

          next_character: CHARACTER

          The character at position+1.

          require

          • valid_next_character

          ensure

          • definition: Result = scanned_string.item(position + 1)

          end_of_input: BOOLEAN

          True when all the characters of 'scanned_string' are scanned.

          ensure

          • implies_last_character_not_valid: Result implies not valid_last_character

          goto_position (pos: INTEGER)

          Change the currently scanned position to 'pos'. Updates 'last_character' and 'valid_last_character' to reflect the new position value.

          require

          • has_no_error: not has_error
          • scanned_string /= Void

          ensure

          • has_no_error: not has_error
          • position_set: position = pos
          • validity_updated: valid_last_character = scanned_string.valid_index(position)
          • character_updated: valid_last_character implies last_character = scanned_string.item(position)

          read_character

          Reads the next character.

          require

          • has_no_error: not has_error
          • not_at_end: not end_of_input

          ensure

          • next_position: position > old position
          • has_no_error: not has_error

          read_integer

          Reads an integer value beginning at the currently scanned position. The readen value is stored in 'last_integer'.

          require

          • has_no_error: not has_error
          • not_at_end: not end_of_input
          • begin_with_a_digit: last_character.is_decimal_digit

          ensure

          • has_no_error: not has_error
          • digits_eaten: end_of_input or else not last_character.is_decimal_digit

          saved_position: INTEGER

          The saved position (only one is currently enougth).

          save_position

          Saves the current scanning position.

          require

          • not_at_end: not end_of_input

          ensure

          • not_at_end: not end_of_input
          • position_kept: position = old position
          • saved_position_set: saved_position = position

          restore_saved_position

          Restore the scanning position to the last saved one.

          ensure

          • position_restored: position = old saved_position
          • not_at_end: not end_of_input

          last_string: STRING

          A string buffer.

          last_integer: INTEGER

          An integer buffer.

          Class invariant