NUMERIC (interface)

Class Interface

indexing
  description: "Objects to which numerical operations are applicable";
  note: "The model is that of a commutative ring."
 
deferred class interface NUMERIC
 
feature -- Access
 
  one: like Current
      -- Neutral element for "*" and "/"
    deferred
    ensure
      Result_exists: Result /= Void
 
  zero: like Current
      -- Neutral element for "+" and "-"
    deferred
    ensure
      Result_exists: Result /= Void
 
feature -- Status report
 
  divisible (other: like Current): BOOLEAN
      -- May current object be divided by other?
    require
      other_exists: other /= Void
    deferred
 
  exponentiable (other: NUMERIC): BOOLEAN
      -- May current object be elevated to the power other?
    require
      other_exists: other /= Void
    deferred
 
  is_special_case: BOOLEAN
      -- Is current object a special case regarding numeric operations?
      -- Special cases are cases where normal mathematical rules don't
      -- apply. Mostly this happens because of the binary represantation 
      -- of the numeric.
    deferred
 
feature -- Basic operations
 
  infix "+" (other: like Current): like Current
      -- Sum with other (commutative).
    require
      other_exists: other /= Void
    deferred
    ensure
      result_exists: Result /= Void;
      commutative: equal (Result, other + Current)
 
  infix "-" (other: like Current): like Current
      -- Result of subtracting other
    require
      other_exists: other /= Void
    deferred
    ensure
      result_exists: Result /= Void
 
  infix "*" (other: like Current): like Current
      -- Product by other
    require
      other_exists: other /= Void
    deferred
    ensure
      result_exists: Result /= Void
 
  infix "/" (other: like Current): like Current
      -- Division by other
    require
      other_exists: other /= Void;
      good_divisor: divisible (other)
    deferred
    ensure
      result_exists: Result /= Void
 
  infix "^" (other: NUMERIC): NUMERIC
      -- Current object to the power other
    require
      other_exists: other /= Void;
      good_exponent: exponentiable (other)
    deferred
    ensure
      result_exists: Result /= Void
 
  prefix "+": like Current
      -- Unary plus
    deferred
    ensure
      result_exists: Result /= Void
 
  prefix "-": like Current
      -- Unary minus
    deferred
    ensure
      result_exists: Result /= Void
 
invariant
 
  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: divisible not is_special_case implies (Current) implies equal (Current / Current, one)

Changes to ELKS 95

new features:

• is_special_case

changed invariants:

• all