class interface P_INTEGER_DECODER creation make (new_base: INTEGER) require ok: new_base > 2 feature(s) from P_INTEGER_DECODER -- Creation make (new_base: INTEGER) require ok: new_base > 2 feature(s) from P_INTEGER_DECODER -- Base base: INTEGER feature(s) from P_INTEGER_DECODER -- Integer extend (digit: CHARACTER) -- Add right digit. require base: is_digit(digit) ensure done_integer: value = old value * base + char_to_int(digit); done_digits: digits = old digits + 1 reset ensure ok: value = 0 and digits = 0 value: INTEGER -- Current integer. digits: INTEGER -- Number of converted digits (not including sign). feature(s) from P_INTEGER_DECODER -- String to integer from_string (str: STRING) require ok: str /= Void feature(s) from P_INTEGER_DECODER -- Digit level int_to_char (digit: INTEGER): CHARACTER -- Integer to character digit. require ok: digit >= 0 and digit < base ensure good_base: is_digit(Result); done: char_to_int(Result) = digit char_to_int (c: CHARACTER): INTEGER -- Character to integer. require is_intchar: is_digit(c) ensure good_base: Result >= 0 and Result < base; -- (case sensitive) int_to_char(Result) = c done: is_digit (c: CHARACTER): BOOLEAN -- Is this character a valid digit? feature(s) from P_INTEGER_DECODER -- Encode value_to_string (int: INTEGER): STRING -- Encode character. ensure is_copy: Result /= Void; done: Result.count > 0 invariant base_ok: base >= 2 and base <= digit_table.count; end of P_INTEGER_DECODER