64 lines
1.6 KiB
Plaintext
64 lines
1.6 KiB
Plaintext
note
|
|
description: "Objects that model Times of Day: 00:00:00 - 23:59:59"
|
|
author: "Eiffel Software Construction Students"
|
|
|
|
class interface
|
|
TIME_OF_DAY
|
|
|
|
create
|
|
make
|
|
|
|
feature -- Initialization
|
|
|
|
make
|
|
-- Initialize to 00:00:00
|
|
ensure
|
|
initialized: hour = 0 and minute = 0 and second = 0
|
|
|
|
feature -- Access
|
|
|
|
hour: INTEGER_32
|
|
-- Hour expressed as 24-hour value
|
|
|
|
minute: INTEGER_32
|
|
-- Minutes past the hour
|
|
|
|
second: INTEGER_32
|
|
-- Seconds past the minute
|
|
|
|
feature -- Element change
|
|
|
|
set_hour (h: INTEGER_32)
|
|
-- Set the hour from `h'
|
|
require
|
|
argument_hour_valid: 0 <= h and h <= 23
|
|
ensure
|
|
hour_set: hour = h
|
|
minute_unchanged: minute = old minute
|
|
second_unchanged: second = old second
|
|
|
|
set_minute (m: INTEGER_32)
|
|
-- Set the minute from `m'
|
|
require
|
|
argument_minute_valid: 0 <= m and m <= 59
|
|
ensure
|
|
minute_set: minute = m
|
|
hour_unchanged: hour = old hour
|
|
second_unchanged: second = old second
|
|
|
|
set_second (s: INTEGER_32)
|
|
-- Set the second from `s'
|
|
require
|
|
argument_second_valid: 0 <= s and s <= 59
|
|
ensure
|
|
second_set: second = s
|
|
hour_unchanged: hour = old hour
|
|
minute_unchanged: minute = old minute
|
|
|
|
invariant
|
|
hour_valid: 0 <= hour and hour <= 23
|
|
minute_valid: 0 <= minute and minute <= 59
|
|
second_valid: 0 <= second and second <= 59
|
|
|
|
end -- class TIME_OF_DAY
|