class interface P_FORMAT
feature(s) from P_FORMAT
-- Misc character (character set independent)
is_hexdigit (ch: CHARACTER): BOOLEAN
-- Is this character hexadecimal? [0-9a-fA-F]
is_digit (ch: CHARACTER): BOOLEAN
-- Is this character a digit? [0-9]
is_alpha (ch: CHARACTER): BOOLEAN
-- Is this character an ASCII alphabetic character? [a-zA-Z]
is_lower (ch: CHARACTER): BOOLEAN
-- Is this character [a-z]?
is_upper (ch: CHARACTER): BOOLEAN
-- Is this character [A-Z]?
feature(s) from P_FORMAT
-- CHARACTER -- ascii case
to_lower (ch: CHARACTER): CHARACTER
-- Convert ASCII character to lower case (strictly a-z).
ensure
done: not is_upper(Result);
down: is_upper(ch) implies is_lower(Result);
keep: not is_upper(ch) implies ch = Result
to_upper (ch: CHARACTER): CHARACTER
-- Convert ASCII character to upper case (stricly A-Z).
ensure
done: not is_lower(Result);
up: is_lower(ch) implies is_upper(Result);
keep: not is_lower(ch) implies ch = Result
feature(s) from P_FORMAT
-- CHARACTER/INTEGER
code_to_char (code: INTEGER): CHARACTER
-- Convert character code (integer) to CHARACTER object.
ensure
done: Result.code = code
feature(s) from P_FORMAT
-- INTEGER/STRING
int_to_str (int: INTEGER): STRING
-- Convert integer to string.
-- Format: "[-](digits)+"
ensure
is_copy: Result /= Void
int_to_str_min (int: INTEGER; min: INTEGER): STRING
-- Convert integer to string,
-- fill with 0 to go up to 'min' digits.
require
min_positive: min >= 0
ensure
min: Result.count >= min;
is_copy: Result /= Void
int_to_hex (int: INTEGER): STRING
-- Convert integer to string, hexadecimal format.
ensure
is_copy: Result /= Void
int_to_hex_min (int: INTEGER; min: INTEGER): STRING
-- Convert integer to string, hexadecimal format.
-- fill with 0 to go up to 'min' digits.
ensure
min: Result.count >= min;
is_copy: Result /= Void
str_to_int (str: STRING): INTEGER
-- Convert string to integer.
-- Format: "[+|-](digits)*"
require
valid: str /= Void
feature(s) from P_FORMAT
-- REAL/STRING, DOUBLE/STRING
str_to_double (str: STRING): DOUBLE
-- String to DOUBLE.
-- Format: "[+|-](digits)*[.[(digits)*]][{e|E}[{+|-}](digits)*]"
require
valid: str /= Void
real_to_str (r: REAL): STRING
-- Convert REAL to string.
-- Format: "[-]E"
ensure
is_copy: Result /= Void
str_to_real (str: STRING): REAL
-- Convert string to REAL.
require
valid: str /= Void
double_to_str (r: DOUBLE): STRING
-- Convert DOUBLE to string.
ensure
is_copy: Result /= Void
feature(s) from P_FORMAT
-- CHARACTER/INTEGER
char_to_int (ch: CHARACTER): INTEGER
-- Convert digit character (0-9) to INTEGER.
require
valid: -- ch should be '0'/'9', otherwise Result = 0
ensure
done: Result >= 0 and Result < 10
int_to_char (int: INTEGER): CHARACTER
-- Convert 0-9 integer to character.
require
valid: int >= 0 and int < 10
ensure
done: char_to_int(Result) = int
feature(s) from P_FORMAT
-- hexadecimal CHARACTER/INTEGER
hex_to_char (int: INTEGER): CHARACTER
-- Convert hex digit to char.
require
hex: int >= 0 and int < 16
ensure
done: char_to_hex(Result) = int
char_to_hex (ch: CHARACTER): INTEGER
-- Convert hex char to integer.
require
hex: -- ch 0-9A-Za-z
ensure
done: Result >= 0 and Result < 16
feature(s) from P_FORMAT
-- Strings & characters
index_of (str: STRING; ch: CHARACTER): INTEGER
-- Index of first occurence of 'ch' in 'str'.
-- Time: O(str.count)
require
valid: str /= Void
ensure
done: not has_character(str,ch) = Result = 0;
found: Result > 0 implies str.item(Result) = ch
index_of_last (str: STRING; ch: CHARACTER): INTEGER
-- Index of last occurence of 'ch' in 'str'.
-- Time: O(str.count)
require
valid: str /= Void
ensure
done: not has_character(str,ch) = Result = 0;
found: Result > 0 implies str.item(Result) = ch
has_character (str: STRING; ch: CHARACTER): BOOLEAN
-- Does 'str' has 'ch'?
-- Time: O(str.count)
require
valid: str /= Void
feature(s) from P_FORMAT
-- String utilities
tokenize (input: STRING; separators: STRING): P_LIST[STRING]
-- Basic tokeniser for a string, returns a list of tokens
-- made of chars which are not in 'separators'.
require
valid_input: input /= Void;
valid_separator: separators /= Void
ensure
not_void: Result /= Void
start_case_equal (a, b: STRING): BOOLEAN
-- Test case-independently if two strings have equal beginnings.
require
valid: a /= Void and b /= Void
start_equal (a, b: STRING): BOOLEAN
-- Test if two strings have equal beginnings.
require
valid: a /= Void and b /= Void
case_equal (a, b: STRING): BOOLEAN
-- Test case-independently if two strings are equal.
require
valid: a /= Void and b /= Void
invert (str: STRING)
-- Invert string.
-- Time: O(str.count)
require
valid: str /= Void
ensure
done: -- invert(str) = old str
end of P_FORMAT