+
Point of view
All features
expanded class TIME
Summary
top
Time and date facilities: year, month, day, hour and seconds.
Direct parents
Insert list: COMPARABLE, HASHABLE, TIME_HANDLER
Overview
top
Features
{ANY}
  • out: STRING
    Create a new string containing terse printable representation of current object.
{ANY}
Setting:
{ANY}
{ANY}
Setting common time mode (local or universal):
{ANY}
Hashing:
{ANY}
{TIME, FILE_TOOLS, TIME_FORMATTER, MICROSECOND_TIME}
{TIME_HANDLER}
{}
{ANY}
  • infix "<=" (other: TIME): BOOLEAN
    Is Current less than or equal other?
  • infix ">" (other: TIME): BOOLEAN
    Is Current strictly greater than other?
  • infix ">=" (other: TIME): BOOLEAN
    Is Current greater than or equal than other?
  • in_range (lower: TIME, upper: TIME): BOOLEAN
    Return True if Current is in range [lower..upper]
    See also min, max, compare.
  • compare (other: TIME): INTEGER_32
    If current object equal to other, 0 if smaller, -1; if greater, 1.
  • three_way_comparison (other: TIME): INTEGER_32
    If current object equal to other, 0 if smaller, -1; if greater, 1.
  • min (other: TIME): TIME
    Minimum of Current and other.
  • max (other: TIME): TIME
    Maximum of Current and other.
  • bounded_by (a_min: TIME, a_max: TIME): TIME
    A value that is equal to Current if it is between the limits set by a_min and a_max.
out: STRING
effective function
{ANY}
top
Create a new string containing terse printable representation of current object.
is_local_time: BOOLEAN
effective function
{ANY}
top
Is the local time in use?
This information applies to all objects of class TIME and MICROSECOND_TIME.
ensure
is_universal_time: BOOLEAN
effective function
{ANY}
top
Is Universal Time in use?
 This information applies to all objects
of class TIME and MICROSECOND_TIME.
ensure
year: INTEGER_32
effective function
{ANY}
top
Number of the year.
month: INTEGER_32
effective function
{ANY}
top
Number of the month (1 for January, 2 for February, ... 12 for December).
ensure
  • Result.in_range(1, 12)
effective function
{ANY}
top
Day of the month in range 1 ..
31.
ensure
  • Result.in_range(1, 31)
hour: INTEGER_32
effective function
{ANY}
top
Hour in range 0..23.
ensure
  • Result.in_range(0, 23)
minute: INTEGER_32
effective function
{ANY}
top
Minute in range 0 ..
59.
ensure
  • Result.in_range(0, 59)
second: INTEGER_32
effective function
{ANY}
top
Second in range 0 ..
59.
ensure
  • Result.in_range(0, 59)
week_day: INTEGER_32
effective function
{ANY}
top
Number of the day in the week (Sunday is 0, Monday is 1, etc.).
ensure
  • Result.in_range(0, 6)
year_day: INTEGER_32
effective function
{ANY}
top
Number of the day in the year in range 0 ..
365.
is_summer_time_used: BOOLEAN
effective function
{ANY}
top
Is summer time in effect?
to_microsecond_time: MICROSECOND_TIME
effective function
{ANY}
top
ensure
  • Result.time.is_equal(Current)
  • Result.microsecond = 0
update
effective procedure
{ANY}
top
Update Current with the current system clock.
set (a_year: INTEGER_32, a_month: INTEGER_32, a_day: INTEGER_32, a_hour: INTEGER_32, a_min: INTEGER_32, sec: INTEGER_32): BOOLEAN
effective function
{ANY}
top
Try to set Current using the given information.
If this input is not a valid date, the Result is False and Current is not updated.
require
  • valid_month: a_month.in_range(1, 12)
  • valid_day: a_day.in_range(1, 31)
  • valid_hour: a_hour.in_range(0, 23)
  • valid_minute: a_min.in_range(0, 59)
  • valid_second: sec.in_range(0, 59)
add_second (s: INTEGER_32)
effective procedure
{ANY}
top
Add s seconds to Current.
require
  • s >= 0
ensure
  • Current >= old Current
add_minute (m: INTEGER_32)
effective procedure
{ANY}
top
Add m minutes to Current.
require
  • m >= 0
ensure
  • Current >= old Current
add_hour (h: INTEGER_32)
effective procedure
{ANY}
top
Add h hours to Current.
require
  • h >= 0
ensure
  • Current >= old Current
add_day (d: INTEGER_32)
effective procedure
{ANY}
top
Add d days to Current.
require
  • d >= 0
ensure
  • Current >= old Current
elapsed_seconds (other: TIME): REAL_64
effective function
{ANY}
top
Elapsed time in seconds from Current to other.
require
  • Current <= other
ensure
  • Result >= 0
is_equal (other: TIME): BOOLEAN
effective function
{ANY}
top
Is other attached to an object considered equal to current object?
require
    • other /= Void
    • other /= Void
ensure
  • Result implies hash_code = other.hash_code
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
  • trichotomy: Result = not Current < other and not other < Current
infix "<" (other: TIME): BOOLEAN
effective function
{ANY}
top
Is Current strictly less than other?
See also >, <=, >=, min, max.
require
  • other_exists: other /= Void
ensure
  • asymmetric: Result implies not other < Current
set_universal_time
effective procedure
{ANY}
top
set_local_time
effective procedure
{ANY}
top
ensure
hash_code: INTEGER_32
effective function
{ANY}
top
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
set_time_memory (tm: INTEGER_64)
effective procedure
{TIME, FILE_TOOLS, TIME_FORMATTER, MICROSECOND_TIME}
top
ensure
time_memory: INTEGER_64
writable attribute
{TIME_HANDLER}
top
The current time value of Current.
As far as we know, this kind of information should always fit into an INTEGER_64.
time_mode_memo: REFERENCE[INTEGER_32]
once function
{}
top
The global default time_mode memory.
time_mode: INTEGER_32
effective function
{}
top
ensure
  • Result = 0 or Result = 1
basic_time: INTEGER_64
{}
top
time_difftime (time2: INTEGER_64, time1: INTEGER_64): REAL_64
{}
top
time_getyear (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_getmonth (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_getday (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_gethour (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_getminute (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_getsecond (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_is_summer_time_used (tm: INTEGER_64): BOOLEAN
{}
top
time_getyday (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_getwday (tm: INTEGER_64, mode: INTEGER_32): INTEGER_32
{}
top
time_mktime (a_year: INTEGER_32, a_mon: INTEGER_32, a_day: INTEGER_32, a_hour: INTEGER_32, a_min: INTEGER_32, a_sec: INTEGER_32): INTEGER_64
{}
top
time_add_second (time: POINTER, s: INTEGER_32)
{}
top
infix "<=" (other: TIME): BOOLEAN
effective function
{ANY}
top
Is Current less than or equal other?
See also >=, <, >, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = Current < other or is_equal(other)
infix ">" (other: TIME): BOOLEAN
effective function
{ANY}
top
Is Current strictly greater than other?
See also <, >=, <=, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = other < Current
infix ">=" (other: TIME): BOOLEAN
effective function
{ANY}
top
Is Current greater than or equal than other?
See also <=, >, <, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = other <= Current
in_range (lower: TIME, upper: TIME): BOOLEAN
effective function
{ANY}
top
Return True if Current is in range [lower..upper]
See also min, max, compare.
ensure
  • Result = Current >= lower and Current <= upper
compare (other: TIME): INTEGER_32
effective function
{ANY}
top
If current object equal to other, 0 if smaller, -1; if greater, 1.
See also min, max, in_range.
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
three_way_comparison (other: TIME): INTEGER_32
effective function
{ANY}
top
If current object equal to other, 0 if smaller, -1; if greater, 1.
See also min, max, in_range.
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
min (other: TIME): TIME
effective function
{ANY}
top
Minimum of Current and other.
See also max, in_range.
require
  • other /= Void
ensure
  • Result <= Current and then Result <= other
  • compare(Result) = 0 or else other.compare(Result) = 0
max (other: TIME): TIME
effective function
{ANY}
top
Maximum of Current and other.
See also min, in_range.
require
  • other /= Void
ensure
  • Result >= Current and then Result >= other
  • compare(Result) = 0 or else other.compare(Result) = 0
bounded_by (a_min: TIME, a_max: TIME): TIME
effective function
{ANY}
top
A value that is equal to Current if it is between the limits set by a_min and a_max.
Otherwise it's a_min if Current is smaller or a_max if Current is greater It's a shortcut for Current.min(a_max).max(a_min) also known as "clamp" in the widespread C library Glib
ensure
  • correctness: Result.in_range(a_min, a_max)