Difference between revisions of "INTEGER (interface)"

m (syntax updated)
m (syntax and feature names updated)
 
Line 57: Line 57:
 
feature -- Comparison
 
feature -- Comparison
  
−
   infix "<" (other: like Current): BOOLEAN
+
   is_less alias "<" (other: like Current): BOOLEAN
 
       -- Is other greater than current integer?
 
       -- Is other greater than current integer?
 
       -- (From COMPARABLE.)
 
       -- (From COMPARABLE.)
Line 65: Line 65:
 
       asymmetric: Result implies not (other < Current)
 
       asymmetric: Result implies not (other < Current)
  
−
   infix "<=" (other: like Current): BOOLEAN
+
   is_less_equal alias "<=" (other: like Current): BOOLEAN
 
       -- Is current object less than or equal to other?
 
       -- Is current object less than or equal to other?
 
       -- (From COMPARABLE.)
 
       -- (From COMPARABLE.)
Line 73: Line 73:
 
       definition: Result = (Current < other) or is_equal (other);
 
       definition: Result = (Current < other) or is_equal (other);
  
−
   infix ">=" (other: like Current): BOOLEAN
+
   is_greater_equal alias ">=" (other: like Current): BOOLEAN
 
       -- Is current object greater than or equal to other?
 
       -- Is current object greater than or equal to other?
 
       -- (From COMPARABLE.)
 
       -- (From COMPARABLE.)
Line 81: Line 81:
 
       definition: Result = (other <= Current)
 
       definition: Result = (other <= Current)
  
−
   infix ">" (other: like Current): BOOLEAN
+
   is_greater alias ">" (other: like Current): BOOLEAN
 
       -- Is current object greater than other?
 
       -- Is current object greater than other?
 
       -- (From COMPARABLE.)
 
       -- (From COMPARABLE.)
Line 152: Line 152:
 
       same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)
 
       same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)
  
−
   infix "*" (other: like Current): like Current
+
   product alias "*" (other: like Current): like Current
 
       -- Product by other
 
       -- Product by other
 
       -- (From NUMERIC.)
 
       -- (From NUMERIC.)
Line 158: Line 158:
 
       other_exists: other /= Void
 
       other_exists: other /= Void
  
−
   infix "+" (other: like Current): like Current
+
   plus alias "+" (other: like Current): like Current
 
       -- Sum with other
 
       -- Sum with other
 
       -- (From NUMERIC.)
 
       -- (From NUMERIC.)
Line 175: Line 175:
 
       result_exists: Result /= Void
 
       result_exists: Result /= Void
  
−
   infix "/" (other: like Current): REAL_64
+
   quotient alias "/" (other: like Current): REAL_64
 
       -- Division by other
 
       -- Division by other
 
     require
 
     require
Line 187: Line 187:
 
       result_correct: not divisble (other) implies Result.is_special_case
 
       result_correct: not divisble (other) implies Result.is_special_case
  
−
   infix "//" (other: like Current): like Current
+
   integer_quotient alias "//" (other: like Current): like Current
 
       -- Integer division of Current by other
 
       -- Integer division of Current by other
 
       -- (From "/" in NUMERIC.)
 
       -- (From "/" in NUMERIC.)
Line 196: Line 196:
 
       result_exists: divisible (other)
 
       result_exists: divisible (other)
  
−
   infix "\\" (other: like Current): like Current
+
   integer_remainder alias "\\" (other: like Current): like Current
 
       -- Remainder of the integer division of Current by other
 
       -- Remainder of the integer division of Current by other
 
     require
 
     require
Line 204: Line 204:
 
       result_exists: Result /= Void
 
       result_exists: Result /= Void
  
−
   infix "^" (other: NUMERIC): REAL_64
+
   power alias "^" (other: NUMERIC): REAL_64
 
       -- Integer power of Current by other
 
       -- Integer power of Current by other
 
       -- (From NUMERIC.)
 
       -- (From NUMERIC.)
Line 213: Line 213:
 
       result_exists: Result /= Void
 
       result_exists: Result /= Void
  
−
   prefix "+": like Current
+
   identity alias "+": like Current
 
       -- Unary plus
 
       -- Unary plus
 
       -- (From NUMERIC.)
 
       -- (From NUMERIC.)
Line 219: Line 219:
 
       result_exists: Result /= Void
 
       result_exists: Result /= Void
  
−
   prefix "-": like Current
+
   opposite alias "-": like Current
 
       -- Unary minus
 
       -- Unary minus
 
       -- (From NUMERIC.)
 
       -- (From NUMERIC.)
Line 233: Line 233:
 
invariant
 
invariant
  
−
   sign_times_abs: not is_special_case implies equal (sign * abs, Current)
+
   sign_times_abs: sign * abs = item
  
 
     -- From COMPARABLE
 
     -- From COMPARABLE

Latest revision as of 12:43, 26 April 2013

Class Interface

note
  description: "Integer values"
 
expanded class interface INTEGER
 
inherit
 
  NUMERIC
 
  COMPARABLE
 
  HASHABLE
 
feature -- Access
 
  hash_code: INTEGER
      -- 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
 
  is_less alias "<" (other: like Current): BOOLEAN
      -- Is other greater than current integer?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      asymmetric: Result implies not (other < Current)
 
  is_less_equal alias "<=" (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);
 
  is_greater_equal alias ">=" (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)
 
  is_greater alias ">" (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)
 
  product alias "*" (other: like Current): like Current
      -- Product by other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
 
  plus alias "+" (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
 
  quotient alias "/" (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
 
  integer_quotient alias "//" (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)
 
  integer_remainder alias "\\" (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
 
  power alias "^" (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
 
  identity alias "+": like Current
      -- Unary plus
      -- (From NUMERIC.)
    ensure
      result_exists: Result /= Void
 
  opposite alias "-": 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: sign * abs = item
 
    -- 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
  • max_value
  • min_value

changed feature contracts:

  • abs
  • infix "/"

changed invariants:

  • sign_times_abs
Retrieved from "https://dev.eiffel.com/index.php?title=INTEGER_(interface)&oldid=14727"