note
	description: "Objects that model Times of Day: 00:00:00 - 23:59:59"
	author: "Eiffel Software Construction Students"

class
    TIME_OF_DAY
create
    make

feature -- Initialization

    make
            -- Initialize to 00:00:00
        do
            hour := 0
            minute := 0
            second := 0
        ensure
            initialized: hour   = 0 and
                    minute = 0 and
                    second = 0
        end

feature -- Access

    hour:   INTEGER
            -- Hour expressed as 24-hour value

    minute: INTEGER
            -- Minutes past the hour

    second: INTEGER
            -- Seconds past the minute

feature -- Element change

    set_hour (h: INTEGER)
            -- Set the hour from `h'
        require
            argument_hour_valid: 0 <= h and h <= 23
        do
            hour := h
        ensure
            hour_set: hour = h
            minute_unchanged: minute = old minute
            second_unchanged: second = old second
        end

    set_minute (m: INTEGER)
            -- Set the minute from `m'
        require
            argument_minute_valid: 0 <= m and m <= 59
        do
            minute := m
        ensure
            minute_set: minute = m
            hour_unchanged: hour = old hour
            second_unchanged: second = old second
        end

    set_second (s: INTEGER)
            -- Set the second from `s'
        require
            argument_second_valid: 0 <= s and s <= 59
        do
            second := s
        ensure
            second_set: second = s
            hour_unchanged: hour = old hour
            minute_unchanged: minute = old minute
        end

feature {NONE} -- Implementation

    protected_routine
            -- A protected routine (not available to client classes)
            -- Will not be present in documentation (Contract) view
        do

        end

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