expanded class interface INTEGER
--
-- 32 bits signed integer.
--
feature(s) from HASHABLE
hash_code: INTEGER
-- The hash-code value of Current.
ensure
good_hash_value: Result >= 0
feature(s) from NUMERIC
infix "+" (other: like Current): like item
-- Sum with other (commutative).
-- require
-- other /= Void
require
no_overflow: item > 0 = (other.item > 0) implies Current #+ other > 0 = (item > 0) -- this means: if operand are of same sign, it will be sign
-- of the Result.
ensure
Result #- other.item = item
infix "-" (other: like Current): like item
-- Result of substracting other.
-- require
-- other /= Void
require
no_overflow: item > 0 /= (other.item > 0) implies Current #- other > 0 = (item > 0) -- this means: if operand are of different sign, sign of the
-- Result will be the same sign as item.
ensure
Result #+ other.item = item
infix "*" (other: like Current): like item
-- Product by other.
-- require
-- other /= Void
require
no_overflow: divisible(other) implies item #* other.item // other.item = item
ensure
item /= 0 and other.item /= 0 implies Result /= 0;
Result /= 0 implies Result // other.item = item;
Result /= 0 implies Result \\ other.item = 0
infix "/" (other: like Current): DOUBLE
-- Division by other.
require
other /= Void;
divisible(other)
prefix "+": like Current
-- Unary plus of Current.
prefix "-": like item
-- Unary minus of Current.
require
not_minimum_value: item = 0 or else item |<< 1 /= 0
divisible (other: like Current): BOOLEAN
-- May Current be divided by other ?
require
other /= Void
one: INTEGER_8
-- Neutral element for "*" and "/".
zero: INTEGER_8
-- Neutral element for "+" and "-".
sign: INTEGER_8
-- Sign of Current (0 -1 or 1).
ensure
-1 <= Result;
Result <= 1
feature(s) from COMPARABLE
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered equal to
-- current object ?
require
other /= Void
ensure
same_dynamic_type(other) implies Result = other.is_equal(Current)
infix "<" (other: like Current): BOOLEAN
-- Is Current strictly less than other?
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
require
other_exists: other /= Void
ensure
definition: Result = (Current < other or is_equal(other))
infix ">" (other: like Current): BOOLEAN
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
in_range (lower, upper: like Current): BOOLEAN
-- Return true if Current is in range [lower..upper]
ensure
Result = (Current >= lower and Current <= upper)
compare (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
min (other: like Current): like Current
-- Minimum of Current and other.
require
other /= Void
ensure
Result <= Current and then Result <= other;
compare(Result) = 0 or else other.compare(Result) = 0
max (other: like Current): like Current
-- Maximum of Current and other.
require
other /= Void
ensure
Result >= Current and then Result >= other;
compare(Result) = 0 or else other.compare(Result) = 0
feature(s) from INTEGER_GENERAL
item: INTEGER
-- Access to the expanded value of Current. (The type of
-- item is INTEGER_8 or INTEGER_16 or INTEGER_32 or INTEGER_64.)
infix "//" (other: like Current): like item
-- Integer division of Current by other
infix "\\" (other: like Current): like item
-- Remainder of integer division of Current by other
infix "^" (exp: like Current): INTEGER_64
-- Integer power of Current by other
require
exp >= 0
abs: like Current
-- Absolute value of Current.
require
not_minimum_value: item = 0 or else item |<< 1 /= 0
odd: BOOLEAN
-- Is odd ?
even: BOOLEAN
-- Is even ?
sqrt: DOUBLE
-- Compute the square routine.
require
item >= 0
log: DOUBLE
-- (ANSI C log).
require
item > 0
log10: DOUBLE
-- (ANSI C log10).
require
item > 0
gcd (other: like Current): like item
-- Great Common Divisor of Current and other.
require
Current >= 0;
other >= 0
ensure
Result.is_equal(other.gcd(Current))
feature(s) from INTEGER_GENERAL
-- Conversions:
to_real: REAL
to_double: DOUBLE
to_string: STRING
-- Convert the decimal view of Current into a new allocated
-- STRING. For example, if Current is -1 the new STRING is "-1".
-- Note: see also append_in to save memory.
to_unicode_string: UNICODE_STRING
-- Convert the decimal view of Current into a new allocated
-- UNICODE_STRING. For example, if Current is -1 the new
-- UNICODE_STRING is U"-1".
-- Note: see also append_in_unicode to save memory.
to_boolean: BOOLEAN
-- Return false for 0, otherwise true.
ensure
Result = (Current.item /= 0)
fit_integer_8: BOOLEAN
-- Does Current fit on an INTEGER_8 ?
ensure
Result = Current.in_range(-128,127)
to_integer_8: INTEGER_8
-- Explicit conversion to INTEGER_8.
require
fit_integer_8
ensure
Current.is_equal(Result)
fit_integer_16: BOOLEAN
-- Does Current fit on an INTEGER_16 ?
ensure
Result = Current.in_range(-32768,32767)
to_integer_16: INTEGER_16
-- Explicit conversion to INTEGER_16.
require
fit_integer_16
ensure
Current.is_equal(Result)
fit_integer_32: BOOLEAN
-- Does Current fit on an INTEGER_32 ?
fit_integer: BOOLEAN
-- Does Current fit on an INTEGER_32 ?
to_integer_32: INTEGER_32
-- Explicit conversion to INTEGER_32.
require
fit_integer_32
ensure
Current.is_equal(Result)
to_integer: INTEGER_32
-- Explicit conversion to INTEGER_32.
require
fit_integer_32
ensure
Current.is_equal(Result)
to_integer_64: INTEGER_64
-- Explicit conversion to INTEGER_64.
ensure
Current.is_equal(Result)
to_number: NUMBER
ensure
Result @= Current.to_integer
to_bit: BIT_N Integer_bits
-- Portable BIT_N conversion.
append_in (buffer: STRING)
-- Append in the buffer the equivalent of to_string. No new
-- STRING creation during the process.
require
buffer /= Void
append_in_unicode (buffer: UNICODE_STRING)
-- Append in the buffer the equivalent of to_unicode_string. No
-- new UNICODE_STRING creation during the process.
require
buffer /= Void
to_string_format (s: INTEGER): STRING
-- Same as to_string but the result is on s character and the
-- number is right aligned.
-- Note: see append_in_format to save memory.
require
to_string.count <= s
ensure
Result.count = s
to_unicode_string_format (s: INTEGER): UNICODE_STRING
-- Same as to_unicode_string but the result is on s character and
-- the number is right aligned.
-- Note: see append_in_unicode_format to save memory.
require
to_string.count <= s
ensure
Result.count = s
append_in_format (str: STRING; s: INTEGER)
-- Append the equivalent of to_string_format at the end of
-- str. Thus you can save memory because no other
-- STRING is allocate for the job.
require
to_string.count <= s
ensure
str.count >= old str.count + s
append_in_unicode_format (str: UNICODE_STRING; s: INTEGER)
-- Append the equivalent of to_unicode_string_format at the end of
-- str. Thus you can save memory because no other
-- UNICODE_STRING is allocate for the job.
require
to_string.count <= s
ensure
str.count >= old str.count + s
decimal_digit: CHARACTER
-- Gives the corresponding CHARACTER for range 0..9.
require
in_range(0,9)
ensure
(once "0123456789").has(Result);
Current.is_equal(Result.value)
digit: CHARACTER
-- Gives the corresponding CHARACTER for range 0..9.
require
in_range(0,9)
ensure
(once "0123456789").has(Result);
Current.is_equal(Result.value)
hexadecimal_digit: CHARACTER
-- Gives the corresponding CHARACTER for range 0..15.
require
in_range(0,15)
ensure
(once "0123456789ABCDEF").has(Result)
to_character: CHARACTER
-- Return the coresponding ASCII character.
require
Current >= 0
to_octal_in (buffer: STRING)
-- Append in buffer the octal view of Current. No new
-- STRING creation during the process.
-- For example, if Current is -1 and if Current is a
-- 16 bits integer the Result is "177777".
-- Note: see also to_hexadecimal_in to save memory.
ensure
buffer.count = old buffer.count + object_size * 8 // 3 + 1
to_hexadecimal: STRING
-- Convert the hexadecimal view of Current into a new allocated
-- STRING. For example, if Current is -1 and if Current is a
-- 32 bits integer the Result is "FFFFFFFF".
-- Note: see also to_hexadecimal_in to save memory.
ensure
Result.count = object_size * 2
to_hexadecimal_in (buffer: STRING)
-- Append in buffer the equivalent of to_hexadecimal. No new
-- STRING creation during the process.
ensure
buffer.count = old buffer.count + object_size * 2
feature(s) from INTEGER_GENERAL
-- Bitwise Logical Operators:
bit_test (idx: INTEGER_8): BOOLEAN
-- The value of the idx-ith bit (the right-most bit is at
-- index 0).
require
idx >= 0
infix "|>>" (s: INTEGER_8): like item
-- Shift by s positions right (sign bit copied) bits falling
-- off the end are lost.
require
s >= 0
bit_shift_right (s: INTEGER_8): like item
-- Shift by s positions right (sign bit copied) bits falling
-- off the end are lost.
require
s >= 0
infix "|>>>" (s: INTEGER_8): like item
-- Shift by s positions right (sign bit not copied) bits
-- falling off the end are lost.
require
s >= 0
bit_shift_right_unsigned (s: INTEGER_8): like item
-- Shift by s positions right (sign bit not copied) bits
-- falling off the end are lost.
require
s >= 0
infix "|<<" (s: INTEGER_8): like item
-- Shift by s positions left bits falling off the end are lost.
require
s >= 0
bit_shift_left (s: INTEGER_8): like item
-- Shift by s positions left bits falling off the end are lost.
require
s >= 0
infix "#>>" (s: INTEGER_8): like item
-- Rotate by s positions right.
require
s >= 0
bit_rotate_right (s: INTEGER_8): like item
-- Rotate by s positions right.
require
s >= 0
infix "#<<" (s: INTEGER_8): like item
-- Rotate by s positions left.
require
s >= 0
bit_rotate_left (s: INTEGER_8): like item
-- Rotate by s positions left.
require
s >= 0
bit_rotate (s: INTEGER_8): like item
-- Rotate by s positions (positive s shifts right, negative left
-- See also infix "#>>" and infix "#<<".
prefix "~": like item
-- One's complement of Current.
bit_not: like item
-- One's complement of Current.
infix "&" (other: like Current): like item
-- Bitwise logical and of Current with other.
bit_and (other: like Current): like item
-- Bitwise logical and of Current with other.
infix "|" (other: like Current): like item
-- Bitwise logical inclusive or of Current with other.
bit_or (other: like Current): like item
-- Bitwise logical inclusive or of Current with other.
bit_xor (other: like Current): like item
-- Bitwise logical exclusive or of Current with other.
bit_shift (s: INTEGER_8): like item
-- Shift by s positions (positive s shifts right (sign bit
-- copied), negative shifts left bits falling off the end are lost).
-- See also infix "|>>" and infix "|<<".
bit_shift_unsigned (s: INTEGER_8): like item
-- Shift by s positions (positive s shifts right (sign bit not
-- copied), negative left bits falling off the end are lost).
-- See also infix "|>>>" and infix "|<<".
feature(s) from INTEGER_GENERAL
-- Object Printing:
out_in_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
ensure
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))
fill_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
feature(s) from INTEGER_GENERAL
-- For experts only: native operators with potential overflow
infix "#+" (other: like Current): like item
infix "#-" (other: like Current): like item
infix "#*" (other: like Current): like item
feature(s) from INTEGER
low_16: INTEGER_16
-- The 16 low bits of Current (i.e. the right-most part).
high_16: INTEGER_16
-- The 16 high bits of Current (i.e. the left-most part).
feature(s) from INTEGER
-- For experts only:
set_item (value: like item)
ensure
item = value
feature(s)
end of expanded INTEGER