class REGULAR_EXPRESSION_STRING_SCANNER

Features exported to ANY

Facility to scan strings TODO improve it by using STRING_HANDLER and string's storage

Direct parents

non-conformant parents

ANY

Known children

non-conformant children

BACKTRACKING_REGULAR_EXPRESSION, BACKTRACKING_REGULAR_EXPRESSION_BUILDER

Summary

exported features

make

basic

error managment

scanning

Details

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