home
wiki
classes/clusters list
class information
+
Point of view
TIME_FORMATTER
ANY
MICROSECOND_TIME
TIME_FORMATTER
FILE_TOOLS
TIME
INTERNALS_HANDLER
All features
expanded class TIME
Summary
top
Time and date facilities: year, month, day, hour and seconds.
Direct parents
insert list:
COMPARABLE
,
HASHABLE
Overview
top
exported features
is_local_time
:
BOOLEAN
Is the local time in use?
is_universal_time
:
BOOLEAN
Is Universal Time in use?
year
:
INTEGER_32
Number of the year.
month
:
INTEGER_32
Number of the month (1 for January, 2 for February, ... 12 for December).
day
:
INTEGER_32
Day of the
month
in range 1 ..
hour
:
INTEGER_32
Hour in range 0..23.
minute
:
INTEGER_32
Minute in range 0 ..
second
:
INTEGER_32
Second in range 0 ..
week_day
:
INTEGER_32
Number of the day in the week (Sunday is 0, Monday is 1, etc.).
year_day
:
INTEGER_32
Number of the day in the year in range 0 ..
is_summer_time_used
:
BOOLEAN
Is summer time in effect?
to_microsecond_time
:
MICROSECOND_TIME
Setting:
update
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
Try to set
Current
using the given information.
add_second
(s:
INTEGER_32
)
Add
s
seconds to
Current
.
add_minute
(m:
INTEGER_32
)
Add
m
minutes to
Current
.
add_hour
(h:
INTEGER_32
)
Add
h
hours to
Current
.
add_day
(d:
INTEGER_32
)
Add
d
days to
Current
.
elapsed_seconds
(other: TIME):
REAL_64
Elapsed time in seconds from
Current
to
other
.
is_equal
(other: TIME):
BOOLEAN
Is
other
attached to an object considered equal to current object?
infix "<"
(other: TIME):
BOOLEAN
Is
Current
strictly less than
other
?
Setting common time mode (local or universal):
set_universal_time
set_local_time
Hashing:
hash_code
:
INTEGER_32
The hash-code value of
Current
.
set_time_memory
(tm:
INTEGER_64
)
time_memory
:
INTEGER_64
The current time value of
Current
.
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
.
is_local_time
:
BOOLEAN
effective function
top
Is the local time in use?
This information applies to all objects of class
TIME
and
MICROSECOND_TIME
.
ensure
Result implies not
is_universal_time
is_universal_time
:
BOOLEAN
effective function
top
Is Universal Time in use?
This information applies to all objects of class
TIME
and
MICROSECOND_TIME
.
ensure
Result implies not
is_local_time
year
:
INTEGER_32
effective function
top
Number of the year.
month
:
INTEGER_32
effective function
top
Number of the month (1 for January, 2 for February, ... 12 for December).
ensure
Result.in_range(1, 12)
day
:
INTEGER_32
effective function
top
Day of the
month
in range 1 ..
31.
ensure
Result.in_range(1, 31)
hour
:
INTEGER_32
effective function
top
Hour in range 0..23.
ensure
Result.in_range(0, 23)
minute
:
INTEGER_32
effective function
top
Minute in range 0 ..
59.
ensure
Result.in_range(0, 59)
second
:
INTEGER_32
effective function
top
Second in range 0 ..
59.
ensure
Result.in_range(0, 59)
week_day
:
INTEGER_32
effective function
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
top
Number of the day in the year in range 0 ..
365.
is_summer_time_used
:
BOOLEAN
effective function
top
Is summer time in effect?
to_microsecond_time
:
MICROSECOND_TIME
effective function
top
ensure
Result.time = Current
Result.microsecond = 0
update
effective procedure
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
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
top
Add
s
seconds to
Current
.
require
s >= 0
ensure
Current
>=
old Current
add_minute
(m:
INTEGER_32
)
effective procedure
top
Add
m
minutes to
Current
.
require
m >= 0
ensure
Current
>=
old Current
add_hour
(h:
INTEGER_32
)
effective procedure
top
Add
h
hours to
Current
.
require
h >= 0
ensure
Current
>=
old Current
add_day
(d:
INTEGER_32
)
effective procedure
top
Add
d
days to
Current
.
require
d >= 0
ensure
Current
>=
old Current
elapsed_seconds
(other: TIME):
REAL_64
effective function
top
Elapsed time in seconds from
Current
to
other
.
require
Current
<=
other
ensure
Result >= 0
is_equal
(other: TIME):
BOOLEAN
effective function
top
Is
other
attached to an object considered equal to current object?
require
other /= Void
ensure
trichotomy:
Result = not Current < other and not other < Current
commutative:
generating_type = other.generating_type implies Result = other.is_equal(Current)
Result implies hash_code = other.hash_code
infix "<"
(other: TIME):
BOOLEAN
effective function
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
top
ensure
is_universal_time
set_local_time
effective procedure
top
ensure
is_local_time
hash_code
:
INTEGER_32
effective function
top
The hash-code value of
Current
.
ensure
good_hash_value:
Result >= 0
set_time_memory
(tm:
INTEGER_64
)
effective procedure
top
ensure
time_memory
= tm
time_memory
:
INTEGER_64
writable attribute
top
The current time value of
Current
.
As far as we know, this kind of information should always fit into an
INTEGER_64
.
infix "<="
(other: TIME):
BOOLEAN
effective function
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
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
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
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
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
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
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
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