expanded class interface DOUBLE
   --
   -- DOUBLE is the type for real numbers with more precision than 'REAL' type.
   -- The precision is not infinite.
   --
   -- Note: An Eiffel DOUBLE is mapped as a C double or as a Java double.
   --

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: like Current): DOUBLE
      -- Sum with other (commutative).
      --      require
      --        other /= Void

   infix "-" (other: like Current): DOUBLE
      -- Result of substracting other.
      --      require
      --         other /= Void

   infix "*" (other: like Current): DOUBLE
      -- Product by other.
      --      require
      --         other /= Void

   infix "/" (other: like Current): DOUBLE
      -- Division by other.
      require
         other /= Void;
         divisible(other)

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

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

   divisible (other: like Current): BOOLEAN
      -- May Current be divided by other ?
      require
         other /= Void

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

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

   sign: INTEGER_8
      -- Sign of Current (0 -1 or 1).
      ensure
         -1 <= Result;
         Result <= 1

feature(s) from COMPARABLE
   is_equal (other: like Current): BOOLEAN
      -- Is other attached to an object considered equal to
      -- current object ?
      require
         other /= Void
      ensure
         trichotomy: Result = (not (Current < other) and not (other < Current));
         generating_type = other.generating_type implies Result = other.is_equal(Current)

   infix "<" (other: like Current): BOOLEAN
      -- Is Current strictly less than other?
      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other < Current)

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

   infix ">" (other: like Current): BOOLEAN
      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

   infix ">=" (other: like Current): BOOLEAN
      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 DOUBLE
   infix "^" (e: INTEGER): DOUBLE
      -- Raise Current to e-th power (see also pow).

   abs: like Current

   double_floor: DOUBLE
      -- Greatest integral value no greater than Current.

   floor: INTEGER
      -- Greatest integral value no greater than Current.
      ensure
         result_no_greater: Result <= Current;
         close_enough: Current - Result < one

   double_ceiling: DOUBLE
      -- Smallest integral value no smaller than Current.

   ceiling: INTEGER
      -- Smallest integral value no smaller than Current.
      ensure
         result_no_smaller: Result >= Current;
         close_enough: Result - Current < one

   rounded: INTEGER
      -- Rounded integral value.

   truncated_to_integer: INTEGER
      -- Integer part (same sign, largest absolute value
      -- no greater than Current).
      ensure
         Result.to_double <= Current

   to_real: REAL
      -- Note: C conversion from "double" to "float".
      -- Thus, Result can be undefine (ANSI C).

   to_string: STRING
      -- Convert the DOUBLE into a new allocated STRING.
      -- As ANSI C, the default number of digit for the
      -- fractionnal part is 6.
      -- Note: see append_in to save memory.

   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 (f: INTEGER): STRING
      -- Convert the DOUBLE into a new allocated STRING including
      -- only f digits in fractionnal part.
      -- Note: see append_in_format to save memory.
      require
         f >= 0

   append_in_format (str: STRING; f: INTEGER)
      -- Same as append_in but produce f digit of
      -- the fractionnal part.
      require
         str /= Void;
         f >= 0

feature(s) from DOUBLE
   -- Maths functions:

   sqrt: DOUBLE
      -- Square root of Current (ANSI C sqrt).
      require
         Current >= 0

   sin: DOUBLE
      -- Sine of Current (ANSI C sin).

   cos: DOUBLE
      -- Cosine of Current (ANSI C cos).

   tan: DOUBLE
      -- Tangent of Current (ANSI C tan).

   asin: DOUBLE
      -- Arc Sine of Current (ANSI C asin).

   acos: DOUBLE
      -- Arc Cosine of Current (ANSI C acos).

   atan: DOUBLE
      -- Arc Tangent of Current (ANSI C atan).

   atan2 (x: DOUBLE): DOUBLE
      -- Arc Tangent of Current / x  (ANSI C atan2).

   sinh: DOUBLE
      -- Hyperbolic Sine of Current (ANSI C sinh).

   cosh: DOUBLE
      -- Hyperbolic Cosine of Current (ANSI C cosh).

   tanh: DOUBLE
      -- Hyperbolic Tangent of Current (ANSI C tanh).

   exp: DOUBLE
      -- Exponential of Current (ANSI C exp).

   log: DOUBLE
      -- Natural Logarithm of Current (ANSI C log).

   log10: DOUBLE
      -- Base-10 Logarithm of Current (ANSI C log10).

   pow (e: DOUBLE): DOUBLE
      -- Current raised to the power of e (ANSI C pow).

feature(s) from DOUBLE
   -- Object Printing:

   out_in_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.
      ensure
         not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
         append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))

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

feature(s) from DOUBLE
   -- For compatibility with the obsolete DOUBLE_REF style:

   item: DOUBLE

   set_item (value: like item)
      ensure
         item = value



end of expanded DOUBLE