View source for INTEGER (interface)

You do not have permission to edit this page, for the following reasons:
The action you have requested is limited to users in one of the groups: Autoconfirmed users, emailconfirmed, editors.
You must confirm your email address before editing pages. Please set and validate your email address through your user preferences.
You can view and copy the source of this page:
[[Category:ELKS]]
__TOC__

==Class Interface==

<code>[eiffel,N]
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
</code>

==Changes to ELKS 95==

new features:
* is_special_case
* max_value
* min_value

changed feature contracts:
* abs
* infix "/"

changed invariants:
* sign_times_abs
Return to INTEGER (interface).
Retrieved from "https://dev.eiffel.com/INTEGER_(interface)"
View source for INTEGER (interface)

Navigation

Development

Wiki

Search

Tools
