expanded class interface MICROSECOND_TIME
   --
   -- Date and time facilities (like TIME) plus an extra microsecond information.
   --

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

      ensure
         good_hash_value: Result >= 0

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
         Result implies elapsed_seconds(other) > 0;
         asymmetric: Result implies not (other < Current)

   infix "<=" (other: like Current): BOOLEAN
      -- Is Current less than or equal other?

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

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

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

   infix ">=" (other: like Current): 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 TIME   is_local_time: BOOLEAN
      -- Is the local time in use? This information applies to all objects
      -- of class TIME and MICROSECOND_TIME.

      ensure
         Result implies not is_universal_time

   is_universal_time: BOOLEAN
      -- Is Universal Time in use?  This information applies to all objects
      -- of class TIME and MICROSECOND_TIME.

      ensure
         Result implies not is_local_time

   year: INTEGER
      -- Number of the year.


   month: INTEGER
      -- Number of the month (1 for January, 2 for February, ...
      -- 12 for December).

      ensure
         Result.in_range(1,12)

   day: INTEGER
      -- Day of the month in range 1 .. 31.

      ensure
         Result.in_range(1,31)

   hour: INTEGER
      -- Hour in range 0..23.

      ensure
         Result.in_range(0,23)

   minute: INTEGER
      -- Minute in range 0 .. 59.

      ensure
         Result.in_range(0,59)

   second: INTEGER
      -- Second in range 0 .. 59.

      ensure
         Result.in_range(0,59)

   week_day: INTEGER
      -- Number of the day in the week (Sunday is 0, Monday is 1, etc.).

      ensure
         Result.in_range(0,6)

   year_day: INTEGER
      -- Number of the day in the year in range 0 .. 365.


   is_summer_time_used: BOOLEAN
      -- Is summer time in effect?


feature(s) from TIME
   -- Setting:

   update
      -- Update Current with the current system clock.


   set (a_year, a_month, a_day, a_hour, a_min, sec: INTEGER): BOOLEAN
      -- Try to set Current using the given information. If this input
      -- is not a valid date, the Result is false and Current is not updated.

      require
         valid_month: a_month.in_range(1,12);
         valid_day: a_day.in_range(1,31);
         valid_hour: a_hour.in_range(0,23);
         valid_minute: a_min.in_range(0,59);
         valid_second: sec.in_range(0,59)

   add_second (s: INTEGER)
      -- Add s seconds to Current.

      ensure
         Current >= old Current

feature(s) from TIME   elapsed_seconds (other: like Current): DOUBLE
      -- Elapsed time in seconds from Current to other with sub-second
      -- precision.

      require
         Current <= other
      ensure
         Result >= 0

feature(s) from TIME
   -- Setting common time mode (local or universal):

   set_universal_time
      ensure
         is_universal_time

   set_local_time
      ensure
         is_local_time

feature(s) from MICROSECOND_TIME   microsecond: INTEGER
      -- Extra information in number of microseconds in range 0 .. 999999.
      -- Note that the accuracy is system dependant.


   to_time: TIME
      ensure
         Result.year = year;
         Result.month = month;
         Result.day = day;
         Result.hour = hour;
         Result.minute = minute;
         Result.second = second

feature(s) from MICROSECOND_TIME
   -- Setting:

   set_microsecond (microsec: INTEGER)
      -- To set microsecond in range 0 .. 999 999.

      require
         microsec.in_range(0,999_999)
      ensure
         microsecond = microsec

   infix "+" (s: DOUBLE): like Current
      -- Add s seconds (2.476 is 2 seconds and 476 milliseconds)

      require
         s >= 0.0

   add_millisecond (millisecond: INTEGER)
      -- Add millisecond milliseconds.

      require
         millisecond.in_range(0,999)
      ensure
         Current >= old Current

   add_microsecond (microsec: INTEGER)
      -- Add microsec microseconds

      require
         microsec.in_range(0,999_999)
      ensure
         Current >= old Current


invariant
   microsecond.in_range(0,999999);

end of expanded MICROSECOND_TIME