expanded class interface DOUBLE
   -- 
   --  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: DOUBLE): DOUBLE
      --  Sum with 'other' (commutative).

      require
         other /= Void

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

      require
         other /= Void

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

      require
         other /= Void

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

      require
         other /= Void;
         divisible(other)

   infix "^" (e: INTEGER): DOUBLE
      --  Raise Current to e-th power (ANSI C pow).

      require
         e >= 0

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


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


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

      require
         other /= Void

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


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


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

      ensure
         - 1 <= Result;
         Result <= 1

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

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

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

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

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

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

   infix ">=" (other: DOUBLE): BOOLEAN
      --  Is Current greater than 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 DOUBLE_REF
   item: DOUBLE

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

   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 DOUBLE
   abs: DOUBLE

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


   floor: INTEGER
      --  Greatest integral value no greater than Current.

      ensure
         result_no_greater: Result.to_double <= 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: Current <= Result;
         close_enough: Current - Result < 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 (d: INTEGER): STRING
      --  Convert the DOUBLE into a new allocated STRING including 
      --  only d digits in fractionnal part. 
      --  Note: see append_in_format to save memory.


   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 routine (ANSI C sqrt).

      require
         Current >= 0

   sin: DOUBLE
      --  Sinus (ANSI C sin).


   cos: DOUBLE
      --  Cosinus (ANSI C cos).


   tan: DOUBLE
      --  (ANSI C tan).


   asin: DOUBLE
      --  (ANSI C asin).


   acos: DOUBLE
      --  (ANSI C acos).


   atan: DOUBLE
      --  (ANSI C atan).


   sinh: DOUBLE
      --  (ANSI C sinh).


   cosh: DOUBLE
      --  (ANSI C cosh).


   tanh: DOUBLE
      --  (ANSI C tanh).


   exp: DOUBLE
      --  (ANSI C exp).


   log: DOUBLE
      --  (ANSI C log).


   log10: DOUBLE
      --  (ANSI C log10).



end of expanded DOUBLE