| 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 = 0make_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 = msmake_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 = smake_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_dayminute: INTEGER -- Minute -- (From DT_TIME_VALUE.) ensure minute_large_enough: Result >= 0 minute_small_enough: Result < Minutes_in_hoursecond: INTEGER -- Second -- (From DT_TIME_VALUE.) ensure second_large_enough: Result >= 0 second_small_enough: Result < Seconds_in_minutemillisecond: INTEGER -- Millisecond -- (From DT_TIME_VALUE.) ensure millisecond_large_enough: Result >= 0 millisecond_small_enough: Result < 1000second_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 /= Voidinfix "&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 /= Voidduration (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.millisecondset_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 = 0set_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 = msset_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 millisecondset_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 millisecondset_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 millisecondset_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 secondset_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 = sset_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 /= Voidadd_time_duration (a_duration: like time_duration) -- Add a_duration to current time. require a_duration_not_void: a_duration /= Voidadd_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 /= Voidprecise_out: STRING -- Printable representation (hh:mm:ss.sss) -- (From DT_TIME_VALUE.) ensure precise_out_not_void: Result /= Voidtime_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 /= Voidprecise_time_out: STRING -- Printable representation (hh:mm:ss.sss) -- (From DT_TIME_VALUE.) ensure precise_time_out_not_void: Result /= Voidappend_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 /= Voidappend_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 /= Voidappend_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 /= Voidappend_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_monthMax_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
|
Copyright © 2000-2001, Eric
Bezault mailto:ericb@gobosoft.com http://www.gobosoft.com Last Updated: 8 April 2001 |
  |