Class DT_DATE_TIME_DURATION PreviousNext 
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
Copyright © 2000-2001, Eric Bezault
mailto:ericb@gobosoft.com
http://www.gobosoft.com
Last Updated: 9 April 2001
 HomeTocPreviousNext