INTEGER (interface): Difference between revisions

From EiffelStudio: an EiffelSoftware project
Jump to navigation Jump to search
← Older edit
Juliant (talk | contribs)
editors
451 edits
mNo edit summary
Conaclos (talk | contribs)
152 edits
m syntax and feature names updated
 
(3 intermediate revisions by 2 users not shown)
Line 5: Line 5:


<code>[eiffel,N]
<code>[eiffel,N]
indexing
note
   description: "Integer values"
   description: "Integer values"


Line 20: Line 20:
feature -- Access
feature -- Access


   hash_code: INTEGER is
   hash_code: INTEGER
       -- Hash code value
       -- Hash code value
       -- (From HASHABLE.)
       -- (From HASHABLE.)
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): DOUBLE
   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: equal (sign * abs, Current)
   sign_times_abs: sign * abs = item


     -- From COMPARABLE
     -- From COMPARABLE
Line 251: Line 251:
new features:
new features:
* is_special_case
* is_special_case
* max_value
* min_value


changed feature contracts:
changed feature contracts:
* abs
* abs
* infix "/"
* infix "/"
changed invariants:
* sign_times_abs

Latest revision as of 21: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"