INTEGER (interface)

Class Interface

indexing
  description: "Integer values"
 
expanded class interface INTEGER
 
inherit
 
  NUMERIC
 
  COMPARABLE
 
  HASHABLE
 
feature -- Access
 
  hash_code: INTEGER is
      -- Hash code value
      -- (From HASHABLE.)
    ensure
      good_hash_value: Result >= 0
 
  one: like Current
      -- Neutral element for "*" and "/"
      -- (From NUMERIC.)
    ensure
      Result_exists: Result /= Void;
      value: Result = 1
 
  sign: INTEGER
      -- Sign value (0, -1 or 1)
    ensure
      three_way: Result = three_way_comparison (zero)
 
  zero: like Current
      -- Neutral element for "+" and "-"
      -- (From NUMERIC.)
    ensure
      Result_exists: Result /= Void;
      value: Result = 0
 
  max_value: like Current
      -- Maximal integer value
    ensure
      Result_exists: Result /= Void;
 
  min_value: like Current
      -- Minimal integer value
    ensure
      Result_exists: Result /= Void;
 
feature -- Comparison
 
  infix "<" (other: like Current): BOOLEAN
      -- Is other greater than current integer?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      asymmetric: Result implies not (other < Current)
 
  infix "<=" (other: like Current): BOOLEAN
      -- Is current object less than or equal to other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (Current < other) or is_equal (other);
 
  infix ">=" (other: like Current): BOOLEAN
      -- Is current object greater than or equal to other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (other <= Current)
 
  infix ">" (other: like Current): BOOLEAN
      -- Is current object greater than other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (other < Current)
 
  max (other: like Current): like Current
      -- The greater of current object and other
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      current_if_not_smaller: (Current >= other) implies (Result = Current)
      other_if_smaller: (Current < other) implies (Result = other)
 
  min (other: like Current): like Current
      -- The smaller of current object and other
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      current_if_not_greater: (Current <= other) implies (Result = Current)
      other_if_greater: (Current > other) implies (Result = other)
 
  three_way_comparison (other: like Current): INTEGER
      -- If current object equal to other, 0; if smaller,
      -- -1; if greater, 1.
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      equal_zero: (Result = 0) = is_equal (other);
      smaller: (Result = 1) = Current < other;
      greater_positive: (Result = -1) = Current > other
 
feature -- Status report
 
  divisible (other: like Current): BOOLEAN
      -- May current object be divided by other?
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      value: Result = (other /= 0)
 
  exponentiable (other: NUMERIC): BOOLEAN
      -- May current object be elevated to the power other?
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      safe_values: (other.conforms_to (Current) or 
          (other.conforms_to (0.0) and (Current >= 0)))
              implies Result
 
  is_special_case: BOOLEAN
      -- Is current object a special case regarding numeric operations?
      -- (From NUMERIC.)
    ensure then
      min_value_is_special: Result implies Current = min_value
 
feature -- Basic operations
 
  abs: like Current
      -- Absolute value
    ensure
      non_negative: not is_special_case implies Result >= 0;
      same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)
 
  infix "*" (other: like Current): like Current
      -- Product by other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
 
  infix "+" (other: like Current): like Current
      -- Sum with other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void;
      commutative: equal (Result, other + Current)
 
  infix "-" (other: like Current): like Current
      -- Result of subtracting other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void
 
  infix "/" (other: like Current): REAL_64
      -- Division by other
    require
      other_exists: other /= Void;
      good_divisor: divisible (other)
    require else
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void
    ensure then
      result_correct: not divisble (other) implies Result.is_special_case
 
  infix "//" (other: like Current): like Current
      -- Integer division of Current by other
      -- (From "/" in NUMERIC.)
    require
      other_exists: other /= Void;
      good_divisor: divisible (other)
    ensure
      result_exists: divisible (other)
 
  infix "\\" (other: like Current): like Current
      -- Remainder of the integer division of Current by other
    require
      other_exists: other /= Void;
      good_divisor: divisible (other)
    ensure
      result_exists: Result /= Void
 
  infix "^" (other: NUMERIC): REAL_64
      -- Integer power of Current by other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void;
      good_exponent: exponentiable (other)
    ensure
      result_exists: Result /= Void
 
  prefix "+": like Current
      -- Unary plus
      -- (From NUMERIC.)
    ensure
      result_exists: Result /= Void
 
  prefix "-": like Current
      -- Unary minus
      -- (From NUMERIC.)
    ensure
      result_exists: Result /= Void
 
feature -- Output
 
  out: STRING
      -- Printable representation of current object
      -- (From GENERAL.)
 
invariant
 
  sign_times_abs: not is_special_case implies equal (sign * abs, Current)
 
    -- From COMPARABLE
  irreflexive_comparison: not (Current < Current);
 
    -- From NUMERIC
  neutral_addition: not is_special_case implies equal (Current + zero, Current);
  self_subtraction: not is_special_case implies equal (Current - Current, zero);
  neutral_multiplication: not is_special_case implies equal (Current * one, Current);
  self_division: not is_special_case implies divisible (Current) implies equal (Current / Current, one)
 
end

Changes to ELKS 95

new features:

• is_special_case

changed feature contracts:

• abs
• infix "/"

changed invariants:

• sign_times_abs