Class DT_DATE_TIME

note

description:

    "Date/times (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

inherit

DT_DATE
    DT_ABSOLUTE_TIME
        COMPARABLE
        HASHABLE
    DT_DATE_VALUE
    DT_GREGORIAN_CALENDAR
DT_TIME
    DT_ABSOLUTE_TIME
        COMPARABLE
        HASHABLE
    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.
    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)
        h_large_enough: h >= 0
        h_small_enough: h < Hours_in_day
        mi_large_enough: mi >= 0
        mi_small_enough: mi < Minutes_in_hour
        s_large_enough: s >= 0
        s_small_enough: s < Seconds_in_minute
    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 with millisecond precision.
    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)
        h_large_enough: h >= 0
        h_small_enough: h < Hours_in_day
        mi_large_enough: mi >= 0
        mi_small_enough: mi < 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
        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_from_date_time (a_date: DT_DATE; a_time: DT_TIME)
        -- Create a new date time using a_date and a_time.
    require
        a_date_not_void: a_date /= Void
        a_time_not_void: a_time /= Void
    ensure
        year_set: year = a_date.year
        month_set: month = a_date.month
        day_set: day = a_date.day
        hour_set: hour = a_time.hour
        minute_set: minute = a_time.minute
        second_set: second = a_time.second
        millisecond_set: millisecond = a_time.millisecond

make_from_date (a_date: DT_DATE)
        -- Create a new date time using a_date.
    require
        a_date_not_void: a_date /= Void
    ensure
        year_set: year = a_date.year
        month_set: month = a_date.month
        day_set: day = a_date.day
        hour_set: hour = 0
        minute_set: minute = 0
        second_set: second = 0
        millisecond_set: millisecond = 0

make_from_epoch (s: INTEGER)
        -- Create a new date time from the number of
        -- seconds since epoch (1 Jan 1970 at 00:00:00).

feature -- Access

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

month: INTEGER
        -- Month
        -- (From DT_DATE_VALUE.)
    ensure
        month_large_enough: Result >= January
        month_small_enough: Result <= December

day: INTEGER
        -- Day
        -- (From DT_DATE_VALUE.)
    ensure
        day_large_enough: Result >= 1
        day_small_enough: Result <= days_in_month (month, year)

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

year_day: INTEGER
        -- Day in current year
        -- (From DT_DATE.)
    ensure
        non_leap_year: not is_leap_year implies (Result >= 1 and Result <= Days_in_year)
        leap_year: is_leap_year implies (Result >= 1 and Result <= Days_in_leap_year)

week_day: INTEGER
        -- Day in current week
        -- (From DT_DATE.)
    ensure
        valid_day: Result >= Sunday and Result <= Saturday

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

millisecond_count: INTEGER
        -- Number of milliseconds since midnight
        -- (From DT_TIME.)
    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 "&d" (a_duration: like date_duration): like Current
        -- Addition of a_duration to current date time
        -- (Create a new object at each call.)
        -- (From DT_DATE.)
    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 date time
        -- (Create a new object at each call.)
        -- (From DT_TIME.)
    require
        a_duration_not_void: a_duration /= Void
    ensure
        addition_not_void: Result /= Void

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

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

date_duration (other: like Current): DT_DATE_DURATION
        -- Duration between other and current date time
        -- (From DT_DATE.)
    require
        other_not_void: other /= Void
    ensure
        date_duration_not_void: Result /= Void
        definite_duration: Result.is_definite
        definition: (other &d Result).is_equal (Current)

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

day_count: INTEGER
        -- Number of days since epoch (1 Jan 1970)
        -- (From DT_DATE.)

days_in_current_month: INTEGER
        -- Number of days in current month
        -- (From DT_DATE.)
    ensure
        at_least_one: Result >= 1
        max_days_in_month: Result <= Max_days_in_month

days_in_previous_month: INTEGER
        -- Number of days in previous month
        -- (From DT_DATE.)
    ensure
        at_least_one: Result >= 1
        max_days_in_month: Result <= Max_days_in_month

date: DT_DATE
        -- Date part
        -- (From DT_DATE_TIME_VALUE.)
    ensure
        date_not_void: Result /= Void
        year_set: Result.year = year
        month_set: Result.month = month
        day_set: Result.day = day

time: DT_TIME
        -- Time part
        -- (From DT_DATE_TIME_VALUE.)
    ensure
        time_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_leap_year: BOOLEAN
        -- Is year a leap year?
        -- (From DT_DATE.)

feature -- Comparison

infix "<" (other: like Current): BOOLEAN
        -- Is current date 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 date time.
        -- (From GENERAL.)
    require
        other_not_void: other /= Void
        type_identity: same_type (other)
    ensure
        is_equal: is_equal (other)

feature -- Setting

set_date (a_date: DT_DATE)
        -- Set year, month and day from a_date.
        -- (From DT_DATE.)
    require
        a_date_not_void: a_date /= Void
    ensure
        year_set: year = a_date.year
        month_set: month = a_date.month
        day_set: day = a_date.day

set_time (a_time: DT_TIME)
        -- Set hour, minute, second and millisecond from a_time.
        -- (From DT_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_year_month_day (y, m, d: INTEGER)
        -- Set year to y, month to m and day to d.
        -- (From DT_DATE.)
    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)
    ensure
        year_set: year = y
        month_set: month = m
        day_set: day = d

set_year (y: INTEGER)
        -- Set year to y.
        -- (From DT_DATE.)
    require
        leap_year_aware: day <= days_in_month (month, y)
    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.)
    require
        m_large_enough: m >= January
        m_small_enough: m <= December
        leap_year_aware: day <= days_in_month (m, year)
    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.)
    require
        d_large_enough: d >= 1
        d_small_enough: d <= days_in_month (month, year)
    ensure
        day_set: day = d
        same_year: year = old year
        same_month: month = old month

set_day_count (d: INTEGER)
        -- Set day_count to d.
        -- (From DT_DATE.)
    ensure
        day_count_set: day_count = d

set_hour_minute_second (h, m, s: INTEGER)
        -- Set hour to h, minute to m and second to s.
        -- (From DT_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

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.)
    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.
        -- (From DT_TIME.)
    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.
        -- (From DT_TIME.)
    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.
        -- (From DT_TIME.)
    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.
        -- (From DT_TIME.)
    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.
        -- (From DT_TIME.)
    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.
        -- (From DT_TIME.)
    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 date time.
        -- (Add a_duration.year and a_duration.month first, then
        -- set day to day.min (days_in_month (new_month, new_year))
        -- and finally add a_duration.day, a_duration.hour,
        -- a_duration.minute, a_duration.second and
        -- a_duration.millisecond.)
        -- (From DT_ABSOLUTE_TIME.)
    require
        a_duration_not_void: a_duration /= Void

add_date_duration (a_duration: like date_duration)
        -- Add a_duration to current date.
        -- (Add a_duration.year and a_duration.month first, then
        -- set day to day.min (days_in_month (new_month, new_year))
        -- and finally add a_duration.day.)
        -- (From DT_DATE.)
    require
        a_duration_not_void: a_duration /= Void

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

add_years_months_days (y, m, d: INTEGER)
        -- Add y years, m months and d days to current date.
        -- (Add y and m first, then set day to
        -- day.min (days_in_month (new_month, new_year))
        -- and finally add d.)
        -- (From DT_DATE.)

add_years (y: INTEGER)
        -- Add y years to current date.
        -- (From DT_DATE.)
    ensure
        day_adjusted: day = (old day).min (days_in_month (month, year))

add_months (m: INTEGER)
        -- Add m months to current date.
        -- (From DT_DATE.)
    ensure
        day_adjusted: day = (old day).min (days_in_month (month, year))

add_days (d: INTEGER)
        -- Add d days to current date.
        -- (From DT_DATE.)

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

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

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

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

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

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

feature -- Output

out: STRING
        -- Printable representation
        -- (yyyy/mm/dd 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
        -- (yyyy/mm/dd hh:mm:ss.sss)
        -- (From DT_TIME_VALUE.)
    ensure
        precise_out_not_void: Result /= Void

date_out: STRING
        -- Printable representation (yyyy/mm/dd)
        -- (From DT_DATE_VALUE.)
    ensure
        date_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
        -- (yyyy/mm/dd hh:mm:ss[.sss]) 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
        -- (yyyy/mm/dd) 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
        -- (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
        -- (yyyy/mm/dd 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_DATE_TIME

Copyright © 2000-2001, Eric Bezault mailto:ericb@gobosoft.com http://www.gobosoft.com Last Updated: 8 April 2001