indexing
description: "Time Measurable Units"
date: "$Date$"
revision: "$Revision$"
deferred class interface
TIME_MEASUREMENT
feature
fine_second: DOUBLE
hour: INTEGER
Hours_in_day: INTEGER is 24
TIME_CONSTANTS
minute: INTEGER
Minutes_in_hour: INTEGER is 60
TIME_CONSTANTS
second: INTEGER
Seconds_in_day: INTEGER is 86400
TIME_CONSTANTS
Seconds_in_hour: INTEGER is 3600
TIME_CONSTANTS
Seconds_in_minute: INTEGER is 60
TIME_CONSTANTS
time_default_format_string: STRING
TIME_CONSTANTS
feature
set_fine_second (s: DOUBLE)
fine_seconds
require
s_large_enough: s >= 0
s_small_enough: s < seconds_in_minute
ensure
fine_second_set: fine_second = s
set_fractionals (f: DOUBLE)
fractional_secondf
require
f_large_enough: f >= 0
f_small_enough: f < 1
ensure
second_same: second = old second
set_hour (h: INTEGER)
hourh
require
h_large_enough: h >= 0
h_small_enough: h < hours_in_day
ensure
hour_set: hour = h
set_minute (m: INTEGER)
minutem
require
m_large_enough: m >= 0
m_small_enough: m < minutes_in_hour
ensure
minute_set: minute = m
set_second (s: INTEGER)
seconds
require
s_large_enough: s >= 0
s_small_enough: s < seconds_in_minute
ensure
second_set: second = s
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- TIME_MEASUREMENT