Class DT_DATE_TIME_DURATION |

    note

>     description:

>         "Date/time durations (Gregorian calendar)"

>     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_DATE_TIME_DURATION

    inherit

>     DT_DATE_DURATION
>         DT_DURATION
>             KL_PART_COMPARABLE
>             HASHABLE
>             KL_CLONABLE
>         DT_DATE_VALUE
>         DT_GREGORIAN_CALENDAR
>     DT_TIME_DURATION
>         DT_DURATION
>             KL_PART_COMPARABLE
>             HASHABLE
>             KL_CLONABLE
>         DT_TIME_VALUE
>         DT_GREGORIAN_CALENDAR
>     DT_DATE_TIME_VALUE
>         DT_DATE_VALUE
>         DT_TIME_VALUE

    create

>     make (y, m, d, h, mi, s: INTEGER)
>             -- Create a new date time duration.
>         ensure
>             year_set: year = y
>             month_set: month = m
>             day_set: day = d
>             hour_set: hour = h
>             minute_set: minute = mi
>             second_set: second = s
>             millisecond_set: millisecond = 0

>     make_precise (y, m, d, h, mi, s, ms: INTEGER)
>             -- Create a new date time duration with millisecond precision.
>         ensure
>             year_set: year = y
>             month_set: month = m
>             day_set: day = d
>             hour_set: hour = h
>             minute_set: minute = mi
>             second_set: second = s
>             millisecond_set: millisecond = ms

>     make_definite (d, h, mi, s: INTEGER)
>             -- Create a new definite date time duration.
>         ensure
>             is_definite: is_definite
>             day_set: day = d
>             hour_set: hour = h
>             minute_set: minute = mi
>             second_set: second = s
>             millisecond_set: millisecond = 0

>     make_precise_definite (d, h, mi, s, ms: INTEGER)
>             -- Create a new definite date time duration
>             -- with millisecond precision.
>         ensure
>             is_definite: is_definite
>             day_set: day = d
>             hour_set: hour = h
>             minute_set: minute = mi
>             second_set: second = s
>             millisecond_set: millisecond = ms

>     make_canonical_definite (s: INTEGER)
>             -- Create a new definite date time duration
>             -- where the time part is canonical and has
>             -- the same sign as the day part.
>         ensure
>             is_definite: is_definite
>             canonical_time: time_duration.is_canonical
>             second_count_set: s = second_count + day * Seconds_in_day
>             millisecond_set: millisecond = 0

>     make_precise_canonical_definite (ms: INTEGER)
>             -- Create a new definite date time duration
>             -- with millisecond precision, where the time
>             -- part is canonical and has the same sign as
>             -- the day part.
>         ensure
>             is_definite: is_definite
>             canonical_time: time_duration.is_canonical
>             millisecond_count_set: ms = millisecond_count + day * Milliseconds_in_day

>     make_from_date_time_duration (a_date_duration: DT_DATE_DURATION;
>         a_time_duration: DT_TIME_DURATION)
>             -- Create a new date time duration using
>             -- a_date_duration and a_time_duration.
>         require
>             a_date_duration_not_void: a_date_duration /= Void
>             a_time_duration_not_void: a_time_duration /= Void
>         ensure
>             year_set: year = a_date_duration.year
>             month_set: month = a_date_duration.month
>             day_set: day = a_date_duration.day
>             hour_set: hour = a_time_duration.hour
>             minute_set: minute = a_time_duration.minute
>             second_set: second = a_time_duration.second
>             millisecond_set: millisecond = a_time_duration.millisecond

>     make_from_date_duration (a_date_duration: DT_DATE_DURATION)
>             -- Create a new date time duration using a_date_duration.
>         require
>             a_date_duration_not_void: a_date_duration /= Void
>         ensure
>             year_set: year = a_date_duration.year
>             month_set: month = a_date_duration.month
>             day_set: day = a_date_duration.day
>             hour_set: hour = 0
>             minute_set: minute = 0
>             second_set: second = 0
>             millisecond_set: millisecond = 0

    feature -- Access

>     year: INTEGER
>             -- Year
>             -- (From DT_DATE_VALUE.)

>     month: INTEGER
>             -- Month
>             -- (From DT_DATE_VALUE.)

>     day: INTEGER
>             -- Day
>             -- (From DT_DATE_VALUE.)

>     hour: INTEGER
>             -- Hour
>             -- (From DT_TIME_VALUE.)

>     minute: INTEGER
>             -- Minute
>             -- (From DT_TIME_VALUE.)

>     second: INTEGER
>             -- Second
>             -- (From DT_TIME_VALUE.)

>     millisecond: INTEGER
>             -- Millisecond
>             -- (From DT_TIME_VALUE.)

>     second_count: INTEGER
>             -- Total number of seconds
>             -- (From DT_TIME_DURATION.)
>         ensure
>             definition: Result = ((hour * Minutes_in_hour + minute) *
>                 Seconds_in_minute + second + millisecond // 1000)

>     millisecond_count: INTEGER
>             -- Total number of milliseconds
>             -- (From DT_TIME_DURATION.)
>         ensure
>             definition: Result = (((hour * Minutes_in_hour + minute) *
>                 Seconds_in_minute + second) * 1000 + millisecond)

>     date_time (a_date_time: DT_DATE_TIME): DT_DATE_TIME
>             -- Addition of current duration to a_date_time
>             -- (Create a new object at each call.)
>             -- (From absolute_time in DT_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             date_time_not_void: Result /= Void
>             definition: Result.is_equal (a_date_time + Current)

>     date_duration: DT_DATE_DURATION
>             -- Date duration part
>             -- (From date in DT_DATE_TIME_VALUE.)
>         ensure
>             date_duration_not_void: Result /= Void
>             year_set: Result.year = year
>             month_set: Result.month = month
>             day_set: Result.day = day

>     time_duration: DT_TIME_DURATION
>             -- Time duration part
>             -- (From time in DT_DATE_TIME_VALUE.)
>         ensure
>             time_duration_not_void: Result /= Void
>             hour_set: Result.hour = hour
>             minute_set: Result.minute = minute
>             second_set: Result.second = second
>             millisecond_set: Result.millisecond = millisecond

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

    feature -- Status report

>     is_definite: BOOLEAN
>             -- Is current duration independant of the date
>             -- on which it applies (use of day only)
>             -- or not (use of year, month and day)?
>             -- (From DT_DATE_DURATION.)
>         ensure
>             definition: Result = (year = 0 and month = 0)

>     is_canonical (a_date_time: like date_time): BOOLEAN
>             -- Has current duration a canonical form
>             -- when to be added to a_date_time?
>             -- (From DT_DATE_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             positive_definition: Result implies
>     	    ((a_date_time <= a_date_time + Current) implies
>     	        (hour >= 0 and hour < Hours_in_day and
>     	        minute >= 0 and minute < Minutes_in_hour and
>     	        second >= 0 and second < Seconds_in_minute and
>     	        millisecond >= 0 and millisecond < 1000 and
>     	        year >= 0 and month >= 0 and month < Months_in_year and
>     	        day >= 0 and
>     	        ((day >= 0 (a_date_time + Current).day implies
>     	            day < (a_date_time + Current).days_in_previous_month) or
>     	        (day < (a_date_time + Current).day implies
>     	            day < (a_date_time + Current).days_in_current_month))))
>             negative_definition: Result implies
>                 ((a_date_time >= a_date_time + Current) implies
>                     (hour <= 0 and hour > -Hours_in_day and
>                     minute <= 0 and minute > -Minutes_in_hour and
>                     second <= 0 and second > -Seconds_in_minute and
>                     millisecond <= 0 and millisecond > -1000 and
>                     year <= 0 and month <= 0 and month > -Months_in_year and
>                     day <= 0 and day > -(a_date_time + Current).days_in_current_month))

>     is_time_canonical: BOOLEAN
>             -- Has date time duration a canonical time part
>             -- and has the time part same sign as the day part?
>             -- (From is_canonical in DT_TIME_DURATION.)
>         ensure
>             positive_definition: Result implies
>                 (millisecond_count >= 0 implies (hour >= 0 and
>                     minute >= 0 and minute < Minutes_in_hour and
>                     second >= 0 and second < Seconds_in_minute and
>                     millisecond >= 0 and millisecond < 1000 and day >= 0))
>             negative_definition: Result implies
>                 (millisecond_count <= 0 implies (hour <= 0 and
>                     minute <= 0 and minute > -Minutes_in_hour and
>                     second <= 0 and second > -Seconds_in_minute and
>                     millisecond <= 0 and millisecond > -1000 and day <= 0))

    feature -- Status setting

>     set_definite (a_date_time: like date_time)
>             -- Set current duration to be definite
>             -- when to be added to a_date_time.
>             -- (From DT_DATE_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             is_definite: is_definite
>             same_duration: (a_date_time + Current).is_equal (a_date_time + old cloned_object)

>     set_canonical (a_date_time: like date_time)
>             -- Set current duration to be canonical
>             -- when to be added to a_date_time.
>             -- (From DT_DATE_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             is_canonical: is_canonical (a_date_time)
>             same_duration: (a_date_time + Current).is_equal (a_date_time + old cloned_object)

>     set_time_canonical
>             -- Set duration with its time part canonical
>             -- and with the same sign as its day part.
>             -- (From set_time_canonical in DT_TIME_DURATION.)
>         ensure
>             is_canonical: is_canonical
>             same_duration: is_equal (old cloned_object)
>             same_year: year = old year
>             same_month: month = old month

    feature -- Setting

>     set_date_duration (a_date_duration: DT_DATE_DURATION)
>             -- Set date part of current date time duration.
>         require
>             a_date_duration_not_void: a_date_duration /= Void
>         ensure
>             year_set: year = a_date_duration.year
>             month_set: month = a_date_duration.month
>             day_set: day = a_date_duration.day

>     set_time_duration (a_time_duration: DT_TIME_DURATION)
>             -- Set time part of current date time duration.
>         require
>             a_time_duration_not_void: a_time_duration /= Void
>         ensure
>             hour_set: hour = a_time_duration.hour
>             minute_set: minute = a_time_duration.minute
>             second_set: second = a_time_duration.second
>             millisecond_set: millisecond = a_time_duration.millisecond

>     set_year_month_day (y, m, d: INTEGER)
>             -- Set year to y, month to m and day to d.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             year_set: year = y
>             month_set: month = m
>             day_set: day = d

>     set_year (y: INTEGER)
>             -- Set year to y.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             year_set: year = y
>             same_month: month = old month
>             same_day: day = old day

>     set_month (m: INTEGER)
>             -- Set month to m.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             month_set: month = m
>             same_year: year = old year
>             same_day: day = old day

>     set_day (d: INTEGER)
>             -- Set day to d.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             day_set: day = d
>             same_year: year = old year
>             same_month: month = old month

>     set_hour_minute_second (h, m, s: INTEGER)
>             -- Set hour to h, minute to m and second to s.
>             -- (From DT_TIME_DURATION.)
>         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.
>             -- (From DT_TIME_DURATION.)
>         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.
>             -- (From DT_TIME_DURATION.)
>         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.
>             -- (From DT_TIME_DURATION.)
>         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.
>             -- (From DT_TIME_DURATION.)
>         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.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             millisecond_set: millisecond = ms
>             same_hour: hour = old hour
>             same_minute: minute = old minute
>             same_second: second = old second

    feature -- Element change

>     add_years_months_days (y, m, d: INTEGER)
>             -- Add y years, m months and d days to current duration.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             years_added: year = old year + y
>             months_added: month = old month + m
>             days_added: day = old day + d

>     add_years (y: INTEGER)
>             -- Add y years to current duration.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             years_added: year = old year + y

>     add_months (m: INTEGER)
>             -- Add m months to current duration.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             months_added: month = old month + m

>     add_days (d: INTEGER)
>             -- Add d days to current duration.
>             -- (From DT_DATE_DURATION.)
>         ensure
>             days_added: day = old day + d

>     add_hours_minutes_seconds (h, m, s: INTEGER)
>             -- Add h hours, m minutes and
>             -- s seconds to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             hour_added: hour = old hour + h
>             minute_added: minute = old minute + m
>             second_added: second = old second + s

>     add_precise_hours_minutes_seconds (h, m, s, ms: INTEGER)
>             -- Add h hours, m minutes, s seconds
>             -- and ms milliseconds to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             hour_added: hour = old hour + h
>             minute_added: minute = old minute + m
>             second_added: second = old second + s
>             millisecond_added: millisecond = old millisecond + ms

>     add_hours (h: INTEGER)
>             -- Add h hours to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             hour_added: hour = old hour + h

>     add_minutes (m: INTEGER)
>             -- Add m minutes to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             minute_added: minute = old minute + m

>     add_seconds (s: INTEGER)
>             -- Add s seconds to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             second_added: second = old second + s

>     add_milliseconds (ms: INTEGER)
>             -- Add ms milliseconds to current duration.
>             -- (From DT_TIME_DURATION.)
>         ensure
>             millisecond_added: millisecond = old millisecond + ms

    feature -- Basic operations

>     infix "+" (other: like Current): like Current
>             -- Sum of current duration with other
>             -- (From DT_DURATION.)
>         require
>             other_not_void: other /= Void
>         ensure
>             addition_not_void: Result /= Void

>     infix "-" (other: like Current): like Current
>             -- Difference with other
>             -- (From DT_DURATION.)
>         require
>             other_not_void: other /= Void
>         ensure
>             subtraction_not_void: Result /= Void

>     prefix "+": like Current
>             -- Unary plus
>             -- (From DT_DURATION.)
>         ensure
>             unary_plus_not_void: Result /= Void
>             same_object: Result = Current

>     prefix "-": like Current
>             -- Unary minus
>             -- (From DT_DURATION.)
>         ensure
>             unary_minus_not_void: Result /= Void

    feature -- Comparison

>     infix "<" (other: like Current): BOOLEAN
>             -- Is current date time duration less than other?
>             -- (From KL_PART_COMPARABLE.)
>         require
>             other_not_void: other /= Void

>     infix "<=" (other: like Current): BOOLEAN
>             -- Is current object less than or equal to other?
>             -- (From KL_PART_COMPARABLE.)
>         require
>             other_not_void: 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 KL_PART_COMPARABLE.)
>         require
>             other_not_void: other /= Void
>         ensure
>             definition: Result = (other <= Current)

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

>     is_equal (other: like Current): BOOLEAN
>             -- Is current date time duration equal to other?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         ensure
>             symmetric: Result implies other.is_equal (Current)
>             consistent: standard_is_equal (other) implies Result

>     same_date_duration (other: DT_DATE_DURATION): BOOLEAN
>             -- Is date part of current duration equal to other?
>             -- (From DT_DATE_DURATION.)
>         require
>             other_not_void: other /= Void
>         ensure
>             definition: Result = ((day = other.day) and
>                 ((year * Months_in_year + month) =
>                     (other.year * Months_in_year + other.month)))

>     same_time_duration (other: DT_TIME_DURATION): BOOLEAN
>             -- Is the time part of current duration equal to other?
>             -- (From DT_TIME_DURATION.)
>         require
>             other_not_void: other /= Void
>         ensure
>             definition: Result = (millisecond_count = other.millisecond_count)

>     same_date_time_duration (other: DT_DATE_TIME_DURATION): BOOLEAN
>             -- Is current date time duration equal to other?
>         require
>             other_not_void: other /= Void
>         ensure
>             definition: Result =
>                 (((day * Milliseconds_in_day + millisecond_count) =
>                     (other.day * Milliseconds_in_day + other.millisecond_count)) and
>                 ((year * Months_in_year + month) =
>                     (other.year * Months_in_year + other.month)))

    feature -- Duplication

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

    feature -- Conversion

>     date_to_date_time_duration: DT_DATE_TIME_DURATION
>             -- Date time duration equivalent to current date duration
>             -- (From to_date_time_duration in DT_DATE_DURATION.)
>         ensure
>             date_time_duration_not_void: Result /= Void
>             year_set: Result.year = year
>             month_set: Result.month = month
>             day_set: Result.day = day
>             hour_set: Result.hour = 0
>             minute_set: Result.minute = 0
>             second_set: Result.second = 0
>             millisecond_set: Result.millisecond = 0

>     time_to_date_time_duration: DT_DATE_TIME_DURATION
>             -- Date time duration equivalent to current time duration
>             -- (From to_date_time_duration in DT_TIME_DURATION.)
>         ensure
>             date_time_duration_not_void: Result /= Void
>             year_set: Result.year = 0
>             month_set: Result.month = 0
>             day_set: Result.day = 0
>             hour_set: Result.hour = hour
>             minute_set: Result.minute = minute
>             second_set: Result.second = second
>             millisecond_set: Result.millisecond = millisecond

>     to_canonical (a_date_time: like date_time): like Current
>             -- Canonical version of current duration
>             -- when to be added to a_date_time
>             -- (From DT_DATE_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             canonical_duration_not_void: Result /= Void
>             is_canonical: Result.is_canonical (a_date_time)
>             same_duration: (a_date_time + Current).is_equal (a_date_time + Result)

>     to_time_canonical : like Current
>             -- Version of current duration where the time part
>             -- is canonical and has the same sign as the day part
>             -- (From to_canonical in DT_TIME_DURATION.)
>         ensure
>             canonical_duration_not_void: Result /= Void
>             is_canonical: Result.is_canonical
>             same_duration: Result.is_equal (Current)
>             same_year: Result.year = year
>             same_month: Result.month = month

>     to_definite (a_date_time: like date_time): like Current
>             -- Definite version of current duration
>             -- when to be added to a_date_time
>             -- (From DT_DATE_DURATION.)
>         require
>             a_date_time_not_void: a_date_time /= Void
>         ensure
>             definite_duration_not_void: Result /= Void
>             is_definite: Result.is_definite
>             same_duration: (a_date_time + Current).is_equal (a_date_time + Result)

    feature -- Output

>     out: STRING
>             -- Printable representation
>             -- (year/month/day hour:minute:second[.millisecond])
>             -- (The millisecond part appears only when not zero.)
>             -- (From GENERAL.)
>         ensure
>             out_not_void: Result /= Void

>     precise_out: STRING
>             -- Printable representation
>             -- (year/month/day hour:minute:second.millisecond)
>             -- (From DT_TIME_VALUE.)
>         ensure
>             precise_out_not_void: Result /= Void

>     date_out: STRING
>             -- Printable representation (year/month/day)
>             -- (From DT_DATE_VALUE.)
>         ensure
>             date_out_not_void: Result /= Void

>     time_out: STRING
>             -- Printable representation (hour:minute:second[.millisecond])
>             -- (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 (hour:minute:second.millisecond)
>             -- (From DT_TIME_VALUE.)
>         ensure
>             precise_time_out_not_void: Result /= Void

>     append_to_string (a_string: STRING)
>             -- Append printable representation
>             -- (year/month/day hour:minute:second[.millisecond])
>             -- to a_string.
>             -- (The millisecond part appears only when not zero.)
>             -- (From DT_TIME_VALUE and DT_DATE_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

>     append_date_to_string (a_string: STRING)
>             -- Append printable representation
>             -- (year/month/day) to a_string.
>             -- (From DT_DATE_VALUE.)
>         require
>             a_string_not_void: a_string /= Void

>     append_time_to_string (a_string: STRING)
>             -- Append printable representation
>             -- (hour:minute:second[.millisecond]) 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
>             -- (year/month/day hour:minute:second.millisecond)
>             --  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
>             -- (hour:minute:second.millisecond) 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)

    end -- class DT_DATE_TIME_DURATION