expanded class TIME

Features exported to TIME_FORMATTER

Time and date facilities: year, month, day, hour and seconds.

Direct parents

conformant parents

COMPARABLE, HASHABLE

Summary

exported features

Setting:

Setting common time mode (local or universal):

Hashing:

Details

is_local_time: BOOLEAN

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

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

Number of the year.

month: INTEGER

Number of the month (1 for January, 2 for February, ... 12 for December).

ensure

  • Result.in_range(1, 12)

day: INTEGER

Day of the month in range 1 .. 31.

ensure

  • Result.in_range(1, 31)

hour: INTEGER

Hour in range 0..23.

ensure

  • Result.in_range(0, 23)

minute: INTEGER

Minute in range 0 .. 59.

ensure

  • Result.in_range(0, 59)

second: INTEGER

Second in range 0 .. 59.

ensure

  • Result.in_range(0, 59)

week_day: INTEGER

Number of the day in the week (Sunday is 0, Monday is 1, etc.).

ensure

  • Result.in_range(0, 6)

year_day: INTEGER

Number of the day in the year in range 0 .. 365.

is_summer_time_used: BOOLEAN

Is summer time in effect?

to_microsecond_time: MICROSECOND_TIME

ensure

  • Result.time = Current
  • Result.microsecond = 0

update

Update Current with the current system clock.

set (a_year: INTEGER, a_month: INTEGER, a_day: INTEGER, a_hour: INTEGER, a_min: INTEGER, sec: INTEGER): BOOLEAN

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)

Add s seconds to Current.

require

  • s >= 0

ensure

  • Current >= old Current

elapsed_seconds (other: TIME): REAL

Elapsed time in seconds from Current to other.

require

  • Current <= other

ensure

  • Result >= 0

is_equal (other: 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: TIME): BOOLEAN

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

ensure

  • is_universal_time

set_local_time

ensure

  • is_local_time

hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

set_time_memory (tm: INTEGER_64)

ensure

  • time_memory = tm

time_memory: INTEGER_64

The current time value of Current. As far as we know, this kind of information should always fit into an INTEGER_64.

deferred is_equal (other: 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: 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: 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: TIME): BOOLEAN

Is Current strictly greater than other?

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

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: 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: TIME, upper: 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: 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: 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: TIME): 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: TIME): 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