expanded class interface INTEGER
   -- 
   --  Note: An Eiffel INTEGER is mapped as a C int or as a Java int.
   -- 

feature(s) from HASHABLE
   hash_code: INTEGER
      --  The hash-code value of Current.

      ensure
         good_hash_value: Result >= 0

feature(s) from NUMERIC
   infix "+" (other: INTEGER): INTEGER
      --  Sum with 'other' (commutative).

      require
         other /= Void

   infix "-" (other: INTEGER): INTEGER
      --  Result of substracting other.

      require
         other /= Void

   infix "*" (other: INTEGER): INTEGER
      --  Product by other.

      require
         other /= Void

   infix "/" (other: INTEGER): DOUBLE
      --  Division by other.

      require
         other /= Void;
         divisible(other)

   infix "^" (exp: INTEGER): INTEGER
      --  Current raised to exp-th power.

      require
         exp >= 0

   prefix "+": INTEGER
      --  Unary plus of Current.


   prefix "-": INTEGER
      --  Unary minus of Current.


   divisible (other: like Current): BOOLEAN
      --  May Current be divided by other ?

      require
         other /= Void

   one: INTEGER
      --  Neutral element for "*" and "/".


   zero: INTEGER
      --  Neutral element for "+" and "-".


   sign: INTEGER
      --  Sign of Current (0 -1 or 1).

      ensure
         - 1 <= Result;
         Result <= 1

   infix "<" (other: INTEGER): BOOLEAN
      --  Is 'Current' strictly less than 'other'?

      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other < Current)

   infix ">" (other: INTEGER): BOOLEAN
      --  Is 'Current' strictly greater than 'other'?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

feature(s) from COMPARABLE
   infix "<=" (other: INTEGER): BOOLEAN
      --  Is 'Current' less or equal 'other'?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (Current < other or is_equal(other))

   infix ">=" (other: INTEGER): BOOLEAN
      --  Is 'Current' greater or equal than 'other'?

      require
         other_exists: other /= Void
      ensure
         definition: Result = (other <= Current)

   in_range (lower, upper: like Current): BOOLEAN
      --  Return true if Current is in range [lower..upper]

      ensure
         Result = (Current >= lower and Current <= upper)

   compare (other: like Current): INTEGER
      --  If current object equal to other, 0;
      --  if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = - 1 = Current < other;
         greater_positive: Result = 1 = Current > other

   three_way_comparison (other: like Current): INTEGER
      --  If current object equal to other, 0;
      --  if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = - 1 = Current < other;
         greater_positive: Result = 1 = Current > other

   min (other: like Current): like Current
      --  Minimum of Current and other.

      require
         other /= Void
      ensure
         Result <= Current and then Result <= other;
         compare(Result) = 0 or else other.compare(Result) = 0

   max (other: like Current): like Current
      --  Maximum of Current and other.

      require
         other /= Void
      ensure
         Result >= Current and then Result >= other;
         compare(Result) = 0 or else other.compare(Result) = 0

feature(s) from INTEGER_REF
   item: INTEGER

feature(s) from INTEGER_REF
   set_item (value: like item)

   infix "//" (other: INTEGER): INTEGER
      --  Integer division by other.

      require
         divisible(other)

   infix "\\" (other: INTEGER): INTEGER
      --  Remainder of integer division by other.

      require
         valid_modulus: divisible(other)

   out_in_tagged_out_memory
      --  Append terse printable represention of current object
      --  in tagged_out_memory.


   fill_tagged_out_memory
      --  Append terse printable represention of current object
      --  in tagged_out_memory.


feature(s) from INTEGER
   abs: INTEGER
      --  Absolute value of Current.


   odd: BOOLEAN
      --  Is odd ?


   even: BOOLEAN
      --  Is even ?


   sqrt: DOUBLE
      --  Compute the square routine.


   log: DOUBLE
      --  (ANSI C log).


   gcd (other: INTEGER): INTEGER
      --  Great Common Divisor of Current and other.

      require
         Current >= 0;
         other >= 0
      ensure
         Result = other.gcd(Current)

feature(s) from INTEGER
   --  Conversions :

   to_real: REAL

   to_double: DOUBLE

   to_string: STRING
      --  Convert the INTEGER into a new allocated STRING. 
      --  Note: see also append_in to save memory.


   to_boolean: BOOLEAN
      --  Return false for 0, otherwise true.

      ensure
         Result = (Current /= 0)

   to_bit: BIT_N Integer_bits
      --  Portable BIT_N conversion.


   append_in (str: STRING)
      --  Append the equivalent of to_string at the end of 
      --  str. Thus you can save memory because no other
      --  STRING is allocate for the job.

      require
         str /= Void

   to_string_format (s: INTEGER): STRING
      --  Same as to_string but the result is on s character and the 
      --  number is right aligned. 
      --  Note: see append_in_format to save memory.

      require
         to_string.count <= s
      ensure
         Result.count = s

   append_in_format (str: STRING; s: INTEGER)
      --  Append the equivalent of to_string_format at the end of 
      --  str. Thus you can save memory because no other
      --  STRING is allocate for the job.

      ensure
         str.count >= old str.count + s

   digit: CHARACTER
      --  Gives the corresponding CHARACTER for range 0..9.

      require
         in_range(0,9)
      ensure
         ("0123456789").has(Result);
         Result.value = Current

   hexadecimal_digit: CHARACTER
      --  Gives the corresponding CHARACTER for range 0..15.

      require
         in_range(0,15)
      ensure
         ("0123456789ABCDEF").has(Result)

   to_character: CHARACTER
      --  Return the coresponding ASCII character.

      require
         Current >= 0

   to_octal: INTEGER
      --  Gives coresponding octal value.



end of expanded INTEGER