home
wiki
classes/clusters list
class information
+
Point of view
ANY
ANY
INTERNALS_HANDLER
All features
expanded class MICROSECOND_TIME
Summary
top
Date and time facilities (like
TIME
) plus an extra microsecond information.
Direct parents
insert list:
COMPARABLE
,
HASHABLE
Class invariant
top
microsecond
.in_range(0, 999999)
Overview
top
exported features
time
:
TIME
The normal
TIME
with second accuracy.
microsecond
:
INTEGER_32
Extra information in number of microseconds in range 0 ..
update
Update
Current
with the current system clock.
set_time
(t:
TIME
)
set_microsecond
(microsec:
INTEGER_32
)
To set
microsecond
in range 0 ..
infix "+"
(s:
REAL_64
): MICROSECOND_TIME
Add
s
seconds (2.476 is 2 seconds and 476 milliseconds)
add_second
(s:
INTEGER_32
)
Add
s
seconds to
Current
.
add_millisecond
(millisecond:
INTEGER_32
)
Add
millisecond
milliseconds.
add_microsecond
(microsec:
INTEGER_32
)
Add
microsec
microseconds
elapsed_seconds
(other: MICROSECOND_TIME):
REAL_64
Elapsed time in seconds from
Current
to
other
with sub-second precision.
is_equal
(other: MICROSECOND_TIME):
BOOLEAN
Is
other
attached to an object considered equal to current object?
infix "<"
(other: MICROSECOND_TIME):
BOOLEAN
Is
Current
strictly less than
other
?
hash_code
:
INTEGER_32
The hash-code value of
Current
.
infix "<="
(other: MICROSECOND_TIME):
BOOLEAN
Is
Current
less than or equal
other
?
infix ">"
(other: MICROSECOND_TIME):
BOOLEAN
Is
Current
strictly greater than
other
?
infix ">="
(other: MICROSECOND_TIME):
BOOLEAN
Is
Current
greater than or equal than
other
?
in_range
(lower: MICROSECOND_TIME, upper: MICROSECOND_TIME):
BOOLEAN
Return True if
Current
is in range [
lower
..
upper
]
See also
min
,
max
,
compare
.
compare
(other: MICROSECOND_TIME):
INTEGER_32
If current object equal to
other
, 0 if smaller, -1; if greater, 1.
three_way_comparison
(other: MICROSECOND_TIME):
INTEGER_32
If current object equal to
other
, 0 if smaller, -1; if greater, 1.
min
(other: MICROSECOND_TIME): MICROSECOND_TIME
Minimum of
Current
and
other
.
max
(other: MICROSECOND_TIME): MICROSECOND_TIME
Maximum of
Current
and
other
.
time
:
TIME
writable attribute
top
The normal
TIME
with second accuracy.
microsecond
:
INTEGER_32
writable attribute
top
Extra information in number of microseconds in range 0 ..
999999. Note that the accuracy is system dependant.
update
effective procedure
top
Update
Current
with the current system clock.
set_time
(t:
TIME
)
effective procedure
top
ensure
time
= t
set_microsecond
(microsec:
INTEGER_32
)
effective procedure
top
To set
microsecond
in range 0 ..
999 999.
require
microsec.in_range(0, 999999)
ensure
microsecond
= microsec
infix "+"
(s:
REAL_64
): MICROSECOND_TIME
effective function
top
Add
s
seconds (2.476 is 2 seconds and 476 milliseconds)
require
s >= 0.0
add_second
(s:
INTEGER_32
)
effective procedure
top
Add
s
seconds to
Current
.
require
s >= 0
ensure
Current
>=
old Current
add_millisecond
(millisecond:
INTEGER_32
)
effective procedure
top
Add
millisecond
milliseconds.
require
millisecond.in_range(0, 999)
ensure
Current
>=
old Current
add_microsecond
(microsec:
INTEGER_32
)
effective procedure
top
Add
microsec
microseconds
require
microsec.in_range(0, 999999)
ensure
Current
>=
old Current
elapsed_seconds
(other: MICROSECOND_TIME):
REAL_64
effective function
top
Elapsed time in seconds from
Current
to
other
with sub-second precision.
is_equal
(other: MICROSECOND_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: MICROSECOND_TIME):
BOOLEAN
effective function
top
Is
Current
strictly less than
other
?
See also
>
,
<=
,
>=
,
min
,
max
.
require
other_exists:
other /= Void
ensure
Result implies
elapsed_seconds
(other) > 0
asymmetric:
Result implies not other < Current
hash_code
:
INTEGER_32
effective function
top
The hash-code value of
Current
.
ensure
good_hash_value:
Result >= 0
infix "<="
(other: MICROSECOND_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: MICROSECOND_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: MICROSECOND_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: MICROSECOND_TIME, upper: MICROSECOND_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: MICROSECOND_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: MICROSECOND_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: MICROSECOND_TIME): MICROSECOND_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: MICROSECOND_TIME): MICROSECOND_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