Difference between revisions of "NUMERIC (interface)"
| m (syntax updated) | |||
| (3 intermediate revisions by one other user not shown) | |||
| Line 4: | Line 4: | ||
| ==Class Interface== | ==Class Interface== | ||
| − | <code> | + | <code> | 
| − | + | note | |
|    description: "Objects to which numerical operations are applicable"; |    description: "Objects to which numerical operations are applicable"; | ||
| − |    note: "The model is that of a  | + |    note: "The model is that of a ring with identity." | 
| deferred class interface NUMERIC | deferred class interface NUMERIC | ||
| Line 40: | Line 40: | ||
|    is_special_case: BOOLEAN |    is_special_case: BOOLEAN | ||
| − |        -- Is current object  | + |        -- Is current object a special case regarding numeric operations? | 
|        -- Special cases are cases where normal mathematical rules don't |        -- Special cases are cases where normal mathematical rules don't | ||
|        -- apply. Mostly this happens because of the binary represantation   |        -- apply. Mostly this happens because of the binary represantation   | ||
| Line 108: | Line 108: | ||
|    self_subtraction: not is_special_case implies equal (Current - Current, zero); |    self_subtraction: not is_special_case implies equal (Current - Current, zero); | ||
|    neutral_multiplication: not is_special_case implies equal (Current * one, Current); |    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) | + |    self_division: divisible not is_special_case implies divisible (Current) implies equal (Current / Current, one) | 
| </code> | </code> | ||
Latest revision as of 13:28, 26 April 2013
Contents
Class Interface
note
  description: "Objects to which numerical operations are applicable";
  note: "The model is that of a ring with identity."
 
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 divisible (Current) implies equal (Current / Current, one)
Changes to ELKS 95
new features:
- is_special_case
changed invariants:
- all


