expanded class MICROSECOND_TIME

Features exported to INTERNALS_HANDLER

Date and time facilities (like TIME) plus an extra microsecond information.

Direct parents

conformant parents

COMPARABLE, HASHABLE

Summary

exported features

Details

time: TIME

The normal TIME with second accuracy.

microsecond: INTEGER

Extra information in number of microseconds in range 0 .. 999999. Note that the accuracy is system dependant.

to_time: TIME
This feature is obsolete: Use simply the `time' feature (june 28th 2004)
update

Update Current with the current system clock.

set_time (t: TIME)

ensure

  • time = t

set_microsecond (microsec: INTEGER)

To set microsecond in range 0 .. 999 999.

require

  • microsec.in_range(0, 999999)

ensure

  • microsecond = microsec

+ (s: REAL): MICROSECOND_TIME

Add s seconds (2.476 is 2 seconds and 476 milliseconds)

require

  • s >= 0.0

add_second (s: INTEGER)

Add s seconds to Current.

require

  • s >= 0

ensure

  • Current >= old Current

add_millisecond (millisecond: INTEGER)

Add millisecond milliseconds.

require

  • millisecond.in_range(0, 999)

ensure

  • Current >= old Current

add_microsecond (microsec: INTEGER)

Add microsec microseconds

require

  • microsec.in_range(0, 999999)

ensure

  • Current >= old Current

elapsed_seconds (other: MICROSECOND_TIME): REAL

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 ?

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

< (other: MICROSECOND_TIME): BOOLEAN

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

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

deferred is_equal (other: MICROSECOND_TIME): BOOLEAN

Is other attached to an object considered equal to current object ?

require

  • other /= Void

ensure

  • Result implies hash_code = other.hash_code
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

is_equal (other: MICROSECOND_TIME): BOOLEAN

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)

<= (other: MICROSECOND_TIME): BOOLEAN

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))

> (other: MICROSECOND_TIME): BOOLEAN

Is Current strictly greater than other?

See also <, >=, <=, min, max.

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: MICROSECOND_TIME): BOOLEAN

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

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

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

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

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

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

Class invariant