Class DT_TIME |

    note

>     description:

>         "Times"

>     remark:       "Do not take leap seconds into account"
>     library:    "Gobo Eiffel Time Library"
>     author:     "Eric Bezault <ericb@gobosoft.com>"
>     copyright:  "Copyright (c) 2000-2001, Eric Bezault and others"
>     license:    "MIT License"

    class interface

>     DT_TIME

    inherit

>     DT_ABSOLUTE_TIME
>         COMPARABLE
>         HASHABLE
>     DT_TIME_VALUE
>     DT_GREGORIAN_CALENDAR

    create

>     make (h, m, s: INTEGER)
>             -- Create a new time.
>         require
>             h_large_enough: h >= 0
>             h_small_enough: h < Hours_in_day
>             m_large_enough: m >= 0
>             m_small_enough: m < Minutes_in_hour
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_minute
>         ensure
>             hour_set: hour = h
>             minute_set: minute = m
>             second_set: second = s
>             millisecond_set: millisecond = 0

>     make_precise (h, m, s, ms: INTEGER)
>             -- Create a new time with millisecond precision.
>         require
>             h_large_enough: h >= 0
>             h_small_enough: h < Hours_in_day
>             m_large_enough: m >= 0
>             m_small_enough: m < Minutes_in_hour
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_minute
>             ms_large_enough: ms >= 0
>             ms_small_enough: ms < 1000
>         ensure
>             hour_set: hour = h
>             minute_set: minute = m
>             second_set: second = s
>             millisecond_set: millisecond = ms

>     make_from_second_count (s: INTEGER)
>             -- Create a new time from the number
>             -- seconds since midnight.
>         require
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_day
>         ensure
>             second_count_set: second_count = s

>     make_from_millisecond_count (ms: INTEGER)
>             -- Create a new time from the number
>             -- milliseconds since midnight.
>         require
>             ms_large_enough: ms >= 0
>             ms_small_enough: ms < Milliseconds_in_day
>         ensure
>             millisecond_count_set: millisecond_count = ms

    feature -- Access

>     hour: INTEGER
>             -- Hour
>             -- (From DT_TIME_VALUE.)
>         ensure
>             hour_large_enough: Result >= 0
>             hour_small_enough: Result < Hours_in_day

>     minute: INTEGER
>             -- Minute
>             -- (From DT_TIME_VALUE.)
>         ensure
>             minute_large_enough: Result >= 0
>             minute_small_enough: Result < Minutes_in_hour

>     second: INTEGER
>             -- Second
>             -- (From DT_TIME_VALUE.)
>         ensure
>             second_large_enough: Result >= 0
>             second_small_enough: Result < Seconds_in_minute

>     millisecond: INTEGER
>             -- Millisecond
>             -- (From DT_TIME_VALUE.)
>         ensure
>             millisecond_large_enough: Result >= 0
>             millisecond_small_enough: Result < 1000

>     second_count: INTEGER
>             -- Number of seconds since midnight
>         ensure
>             definition: Result = (((hour * Minutes_in_hour) + minute) *
>                 Seconds_in_minute + second)

>     millisecond_count: INTEGER
>             -- Number of milliseconds since midnight
>         ensure
>             definition: Result = ((((hour * Minutes_in_hour) + minute) *
>                 Seconds_in_minute + second) * 1000 + millisecond)

>     infix "-" (other: like Current): like duration
>             -- Duration between other and Current
>             -- (From DT_ABSOLUTE_TIME.)
>         require
>             other_not_void: other /= Void
>         ensure
>             duration_not_void: Result /= Void
>             definition: (other + Result).is_equal (Current)

>     infix "+" (a_duration: like duration): like Current
>             -- Addition of a_duration to Current
>             -- (Create a new object at each call.)
>             -- (From DT_ABSOLUTE_TIME.)
>         require
>             a_duration_not_void: a_duration /= Void
>         ensure
>             addition_not_void: Result /= Void

>     infix "&t" (a_duration: like time_duration): like Current
>             -- Addition of a_duration to current time
>             -- (Create a new object at each call.)
>         require
>             a_duration_not_void: a_duration /= Void
>         ensure
>             addition_not_void: Result /= Void

>     duration (other: like Current): DT_TIME_DURATION
>             -- Duration between other and curent time
>             -- (From DT_ABSOLUTE_TIME.)
>         require
>             other_not_void: other /= Void
>         ensure
>             duration_not_void: Result /= Void
>             definition: (other + Result).is_equal (Current)

>     canonical_duration (other: like Current): like duration
>             -- Canonical duration between other and current time
>         require
>             other_not_void: other /= Void
>         ensure
>             duration_not_void: Result /= Void
>             canonical_duration: Result.is_canonical (other)
>             definition: (other + Result).is_equal (Current)

>     time_duration (other: like Current): DT_TIME_DURATION
>             -- Duration between other and current time
>         require
>             other_not_void: other /= Void
>         ensure
>             time_duration_not_void: Result /= Void
>             definition: (other &t Result).is_equal (Current)

>     hash_code: INTEGER
>             -- Hash code value
>             -- (From HASHABLE.)
>         ensure
>             good_hash_value: Result >= 0

    feature -- Comparison

>     infix "<" (other: like Current): BOOLEAN
>             -- Is current time before other on the time axis?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         ensure
>             asymmetric: Result implies not (other < Current)

>     infix "<=" (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))

>     infix ">=" (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)

>     infix ">" (other: like Current): BOOLEAN
>             -- Is current object greater than other?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         ensure
>             definition: Result = (other < Current)

>     is_equal (other: like Current): BOOLEAN
>             -- Is other attached to an object considered equal
>             -- to current object?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         ensure
>             symmetric: Result implies other.is_equal (Current)
>             consistent: standard_is_equal (other) implies Result
>             trichotomy: Result = (not (Current < other) and not (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_negative: (Result = -1) = (Current < other)
>             greater_positive: (Result = 1) = (Current > other)

    feature -- Duplication

>     copy (other: like Current)
>             -- Copy other to current time.
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>             type_identity: same_type (other)
>         ensure
>             is_equal: is_equal (other)

    feature -- Setting

>     set_time (a_time: DT_TIME)
>             -- Set hour, minute, second and millisecond from a_time.
>         require
>             a_time_not_void: a_time /= Void
>         ensure
>             hour_set: hour = a_time.hour
>             minute_set: minute = a_time.minute
>             second_set: second = a_time.second
>             millisecond_set: millisecond = a_time.millisecond

>     set_hour_minute_second (h, m, s: INTEGER)
>             -- Set hour to h, minute to m and second to s.
>         require
>             h_large_enough: h >= 0
>             h_small_enough: h < Hours_in_day
>             m_large_enough: m >= 0
>             m_small_enough: m < Minutes_in_hour
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_minute
>         ensure
>             hour_set: hour = h
>             minute_set: minute = m
>             second_set: second = s
>             millisecond_set: millisecond = 0

>     set_precise_hour_minute_second (h, m, s, ms: INTEGER)
>             -- Set hour to h, minute to m, second
>             -- to s, and millisecond to ms.
>         require
>             h_large_enough: h >= 0
>             h_small_enough: h < Hours_in_day
>             m_large_enough: m >= 0
>             m_small_enough: m < Minutes_in_hour
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_minute
>             ms_large_enough: ms >= 0
>             ms_small_enough: ms < 1000
>         ensure
>             hour_set: hour = h
>             minute_set: minute = m
>             second_set: second = s
>             millisecond_set: millisecond = ms

>     set_hour (h: INTEGER)
>             -- Set hour to h.
>         require
>             h_large_enough: h >= 0
>             h_small_enough: h < Hours_in_day
>         ensure
>             hour_set: hour = h
>             same_minute: minute = old minute
>             same_second: second = old second
>             same_millisecond: millisecond = old millisecond

>     set_minute (m: INTEGER)
>             -- Set minute to m.
>         require
>             m_large_enough: m >= 0
>             m_small_enough: m < Minutes_in_hour
>         ensure
>             minute_set: minute = m
>             same_hour: hour = old hour
>             same_second: second = old second
>             same_millisecond: millisecond = old millisecond

>     set_second (s: INTEGER)
>             -- Set second to s.
>         require
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_minute
>         ensure
>             second_set: second = s
>             same_hour: hour = old hour
>             same_minute: minute = old minute
>             same_millisecond: millisecond = old millisecond

>     set_millisecond (ms: INTEGER)
>             -- Set millisecond to ms.
>         require
>             ms_large_enough: ms >= 0
>             ms_small_enough: ms < 1000
>         ensure
>             millisecond_set: millisecond = ms
>             same_hour: hour = old hour
>             same_minute: minute = old minute
>             same_second: second = old second

>     set_second_count (s: INTEGER)
>             -- Set second_count to s.
>         require
>             s_large_enough: s >= 0
>             s_small_enough: s < Seconds_in_day
>         ensure
>             second_count_set: second_count = s

>     set_millisecond_count (ms: INTEGER)
>             -- Set millisecond_count to ms.
>         require
>             ms_large_enough: ms >= 0
>             ms_small_enough: ms < Milliseconds_in_day
>         ensure
>             millisecond_count_set: millisecond_count = ms

    feature -- Element change

>     add_duration (a_duration: like duration)
>             -- Add a_duration to current time.
>             -- (From DT_ABSOLUTE_TIME.)
>         require
>             a_duration_not_void: a_duration /= Void

>     add_time_duration (a_duration: like time_duration)
>             -- Add a_duration to current time.
>         require
>             a_duration_not_void: a_duration /= Void

>     add_hours_minutes_seconds (h, m, s: INTEGER)
>             -- Add h hours, m minutes and
>             -- s seconds to current time.

>     add_precise_hours_minutes_seconds (h, m, s, ms: INTEGER)
>             -- Add h hours, m minutes, s seconds
>             -- and ms milliseconds to current time.

>     add_hours (h: INTEGER)
>             -- Add h hours to current time.

>     add_minutes (m: INTEGER)
>             -- Add m minutes to current time.

>     add_seconds (s: INTEGER)
>             -- Add s seconds to current time.

>     add_milliseconds (ms: INTEGER)
>             -- Add ms milliseconds to current time.

    feature -- Output

>     out: STRING
>             -- Printable representation (hh:mm:ss[.sss])
>             -- (The millisecond part appears only when not zero.)
>             -- (From GENERAL.)
>         ensure
>             out_not_void: Result /= Void

>     precise_out: STRING
>             -- Printable representation (hh:mm:ss.sss)
>             -- (From DT_TIME_VALUE.)
>         ensure
>             precise_out_not_void: Result /= Void

>     time_out: STRING
>             -- Printable representation (hh:mm:ss[.sss])
>             -- (The millisecond part appears only when not zero.)
>             -- (From DT_TIME_VALUE.)
>         ensure
>             time_out_not_void: Result /= Void

>     precise_time_out: STRING
>             -- Printable representation (hh:mm:ss.sss)
>             -- (From DT_TIME_VALUE.)
>         ensure
>             precise_time_out_not_void: Result /= Void

>     append_to_string (a_string: STRING)
>             -- Append printable representation
>             -- (hh:mm:ss[.sss]) to a_string.
>             -- (The millisecond part appears only when not zero.)
>             -- (From DT_TIME_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

>     append_time_to_string (a_string: STRING)
>             -- Append printable representation
>             -- (hh:mm:ss[.sss]) to a_string.
>             -- (The millisecond part appears only when not zero.)
>             -- (From DT_TIME_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

>     append_precise_to_string (a_string: STRING)
>             -- Append printable representation (hh:mm:ss.sss)
>             -- to a_string.
>             -- (From DT_TIME_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

>     append_precise_time_to_string (a_string: STRING)
>             -- Append printable representation (hh:mm:ss.sss)
>             -- to a_string.
>             -- (From DT_TIME_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

    feature -- Year

>     leap_year (y: INTEGER): BOOLEAN
>             -- Is y a leap year?
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Months_in_year: INTEGER
>             -- Number of months in a year
>             -- (From DT_GREGORIAN_CALENDAR.)
>         ensure
>             definition: Result = (December - Januray + 1)

>     Days_in_year: INTEGER
>     Days_in_leap_year: INTEGER
>             -- Number of days in a (leap) year
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Days_in_400_years: INTEGER
>     Days_in_100_years: INTEGER
>     Days_in_4_years: INTEGER
>     Days_in_3_years: INTEGER
>     Days_in_3_leap_years: INTEGER
>     Days_in_2_years: INTEGER
>     Days_in_2_leap_years: INTEGER
>             -- Number of days in multiple years
>             -- (From DT_GREGORIAN_CALENDAR.)

    feature -- Month

>     January: INTEGER
>     February: INTEGER
>     March: INTEGER
>     April: INTEGER
>     May: INTEGER
>     June: INTEGER
>     July: INTEGER
>     August: INTEGER
>     September: INTEGER
>     October: INTEGER
>     November: INTEGER
>     December: INTEGER
>             -- Months
>             -- (From DT_GREGORIAN_CALENDAR.)

>     days_in_month (m, y: INTEGER): INTEGER
>             -- Number of days in month m of year y
>             -- (From DT_GREGORIAN_CALENDAR.)
>         require
>             m_large_enough: m >= January
>             m_small_enough: m <= December
>         ensure
>             at_least_one: Result >= 1
>             max_days_in_month: Result <= Max_days_in_month

>     Max_days_in_month: INTEGER
>             -- Maximum number of days in a month
>             -- (From DT_GREGORIAN_CALENDAR.)

>     days_at_month (m, y: INTEGER): INTEGER
>             -- Number of days from beginning of year
>             -- y until beginning of month m
>             -- (From DT_GREGORIAN_CALENDAR.)
>         require
>             m_large_enough: m >= January
>             m_small_enough: m <= December
>         ensure
>             days_positive: Result >= 0

    feature -- Week day

>     Sunday: INTEGER
>     Monday: INTEGER
>     Tuesday: INTEGER
>     Wednesday: INTEGER
>     Thursday: INTEGER
>     Friday: INTEGER
>     Saturday: INTEGER
>             -- Week days
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Days_in_week: INTEGER
>             -- Number of days in a week
>             -- (From DT_GREGORIAN_CALENDAR.)
>         ensure
>             definition: Result = (Saturday - Sunday + 1)

>     next_day (d: INTEGER): INTEGER
>             -- Week day after d
>             -- (From DT_GREGORIAN_CALENDAR.)
>         require
>             d_large_enough: d >= Sunday
>             d_small_enough: d <= Saturday
>         ensure
>             sunday_definition: (d = Sunday) implies (Result = Monday)
>             monday_definition: (d = Monday) implies (Result = Tuesday)
>             tuesday_definition: (d = Tuesday) implies (Result = Wednesday)
>             wednesday_definition: (d = Wednesday) implies (Result = Thursday)
>             thursday_definition: (d = Thursday) implies (Result= Friday)
>             friday_definition: (d = Friday) implies (Result = Saturday)
>             saturday_definition: (d = Saturday) implies (Result = Sunday)

>     previous_day (d: INTEGER): INTEGER
>             -- Week day before d
>             -- (From DT_GREGORIAN_CALENDAR.)
>         require
>             d_large_enough: d >= Sunday
>             d_small_enough: d <= Saturday
>         ensure
>             sunday_definition: (d = Sunday) implies (Result = Saturday)
>             monday_definition: (d = Monday) implies (Result = Sunday)
>             tuesday_definition: (d = Tuesday) implies (Result = Monday)
>             wednesday_definition: (d = Wednesday) implies (Result = Tuesday)
>             thursday_definition: (d = Thursday) implies (Result= Wednesday)
>             friday_definition: (d = Friday) implies (Result = Thursday)
>             saturday_definition: (d = Saturday) implies (Result = Friday)

    feature -- Time

>     Seconds_in_minute: INTEGER
>             -- Number of seconds in a minute
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Seconds_in_hour: INTEGER
>             -- Number of seconds in an hour
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Seconds_in_day: INTEGER
>             -- Number of seconds in a day
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Milliseconds_in_day: INTEGER
>             -- Number of milliseconds in a day
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Minutes_in_hour: INTEGER
>             -- Number of minutes in an hour
>             -- (From DT_GREGORIAN_CALENDAR.)

>     Hours_in_day: INTEGER
>             -- Number of hours in a day
>             -- (From DT_GREGORIAN_CALENDAR.)

    feature -- Epoch

>     Epoch_year: INTEGER
>     Epoch_month: INTEGER
>     Epoch_day: INTEGER
>             -- Epoch date (1 Jan 1970)
>             -- (From DT_GREGORIAN_CALENDAR.)

>     epoch_days (y, m, d: INTEGER): INTEGER
>             -- Number of days since epoch date (1 Jan 1970)
>             -- (From DT_GREGORIAN_CALENDAR.)
>         require
>             m_large_enough: m >= January
>             m_small_enough: m <= December
>             d_large_enough: d >= 1
>             d_small_enough: d <= days_in_month (m, y)

    invariant

>     irreflexive_comparison: not (Current < Current)
>         -- (From COMPARABLE.)

    end -- class DT_TIME