indexing
	description: "Absolute times"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"
	access: time

class interface
	TIME

create 

	make (h, m, s: INTEGER)
			-- Set `hour, minute and second to h, m, s respectively.
		require
			correct_time: is_correct_time (h, m, s, False)
		ensure
			hour_set: hour = h
			minute_set: minute = m
			second_set: second = s

	make_fine (h, m: INTEGER; s: DOUBLE)
			-- Set `hour, minute and second to h, m and truncated to
			-- integer part of s respectively.
			-- Set fractional_second to the fractional part of s.
		require
			correct_time: is_correct_time (h, m, s, False)
		ensure
			hour_set: hour = h
			minute_set: minute = m
			fine_second_set: fine_second = s

	make_now
			-- Set current time according to timezone.

	make_by_seconds (sec: INTEGER)
			-- Set the object by the number of seconds sec from midnight.
		require
			s_large_enough: sec >= 0
			s_small_enough: sec < seconds_in_day
		ensure
			seconds_set: seconds = sec

	make_by_fine_seconds (sec: DOUBLE)
			-- Set the object by the number of seconds sec.
		require
			s_large_enough: sec >= 0
			s_small_enough: sec < seconds_in_day

	make_from_string (s: STRING; code: STRING)
			-- Initialize from a "standard" string of form
			-- code.
		require
			s_exists: s /= void
			c_exists: code /= void
			time_valid: time_valid (s, code)

	make_from_string_default (s: STRING)
			-- Initialize from a "standard" string of form
			-- default_format_string.
		require
			s_exists: s /= void
			time_valid: time_valid (s, default_format_string)

	make_by_compact_time (c_t: INTEGER)
			-- Initialize from compact_time.
		require
			c_t_not_void: c_t /= void
			c_t_valid: compact_time_valid (c_t)
		ensure
			compact_time_set: compact_time = c_t

feature -- Initialization

	make (h, m, s: INTEGER)
			-- Set `hour, minute and second to h, m, s respectively.
		require
			correct_time: is_correct_time (h, m, s, False)
		ensure
			hour_set: hour = h
			minute_set: minute = m
			second_set: second = s

	make_by_compact_time (c_t: INTEGER)
			-- Initialize from compact_time.
		require
			c_t_not_void: c_t /= void
			c_t_valid: compact_time_valid (c_t)
		ensure
			compact_time_set: compact_time = c_t

	make_by_fine_seconds (sec: DOUBLE)
			-- Set the object by the number of seconds sec.
		require
			s_large_enough: sec >= 0
			s_small_enough: sec < seconds_in_day

	make_by_seconds (sec: INTEGER)
			-- Set the object by the number of seconds sec from midnight.
		require
			s_large_enough: sec >= 0
			s_small_enough: sec < seconds_in_day
		ensure
			seconds_set: seconds = sec

	make_fine (h, m: INTEGER; s: DOUBLE)
			-- Set `hour, minute and second to h, m and truncated to
			-- integer part of s respectively.
			-- Set fractional_second to the fractional part of s.
		require
			correct_time: is_correct_time (h, m, s, False)
		ensure
			hour_set: hour = h
			minute_set: minute = m
			fine_second_set: fine_second = s

	make_from_string (s: STRING; code: STRING)
			-- Initialize from a "standard" string of form
			-- code.
		require
			s_exists: s /= void
			c_exists: code /= void
			time_valid: time_valid (s, code)

	make_from_string_default (s: STRING)
			-- Initialize from a "standard" string of form
			-- default_format_string.
		require
			s_exists: s /= void
			time_valid: time_valid (s, default_format_string)

	make_now
			-- Set current time according to timezone.
	
feature -- Access

	compact_time: INTEGER
			-- Hour, minute, second coded.
			-- (from TIME_VALUE)

	fine_second: DOUBLE
			-- Representation of second with decimals
			-- (from TIME_VALUE)

	fractional_second: DOUBLE
			-- Fractional part of fine_second
			-- (from TIME_VALUE)

	hour: INTEGER
			-- Hour of the current time
			-- (from TIME_VALUE)

	Hours_in_day: INTEGER is 24
			-- Number of hours in a day
			-- (from TIME_CONSTANTS)

	micro_second: INTEGER
			-- Microsecond of the current time
			-- (from TIME_VALUE)

	milli_second: INTEGER
			-- Millisecond of the current time
			-- (from TIME_VALUE)

	minute: INTEGER
			-- Minute of the current time
			-- (from TIME_VALUE)

	Minutes_in_hour: INTEGER is 60
			-- Number of minutes in an hour
			-- (from TIME_CONSTANTS)

	nano_second: INTEGER
			-- Nanosecond of the current time
			-- (from TIME_VALUE)

	origin: TIME
			-- Origin time
		ensure -- from ABSOLUTE
			result_exists: Result /= void

	second: INTEGER
			-- Second of the current time
			-- (from TIME_VALUE)

	Seconds_in_day: INTEGER is 86400
			-- Number of seconds in an hour
			-- (from TIME_CONSTANTS)

	Seconds_in_hour: INTEGER is 3600
			-- Number of seconds in an hour
			-- (from TIME_CONSTANTS)

	Seconds_in_minute: INTEGER is 60
			-- Number of seconds in a minute
			-- (from TIME_CONSTANTS)

	time_default_format_string: STRING
			-- Default output format for times
			-- (from TIME_CONSTANTS)
	
feature -- Measurement

	duration: TIME_DURATION
			-- Duration elapsed from midnight
		ensure then
			seconds_large_enough: duration.seconds_count >= 0
			seconds_small_enough: duration.seconds_count < seconds_in_day

	fine_seconds: DOUBLE
			-- Number of seconds and fractions of seconds elapsed from midnight

	seconds: INTEGER
			-- Number of seconds elapsed from midnight
		ensure
			result_definition: Result = duration.seconds_count
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is other attached to an object of the same type
			-- as current object and identical to it?
			-- (from COMPARABLE)
		require -- from ANY
			other_not_void: other /= void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result
		ensure then -- from COMPARABLE
			trichotomy: Result = (not (Current < other) and not (other < Current))

	max (other: like Current): like Current
			-- The greater of current object and other
			-- (from COMPARABLE)
		require -- from COMPARABLE
			other_exists: other /= void
		ensure -- from COMPARABLE
			current_if_not_smaller: Current >= other implies Result = Current
			other_if_smaller: Current < other implies Result = other

	min (other: like Current): like Current
			-- The smaller of current object and other
			-- (from COMPARABLE)
		require -- from COMPARABLE
			other_exists: other /= void
		ensure -- from COMPARABLE
			current_if_not_greater: Current <= other implies Result = Current
			other_if_greater: Current > other implies Result = other

	three_way_comparison (other: like Current): INTEGER
			-- If current object equal to other, 0;
			-- if smaller, -1; if greater, 1
			-- (from COMPARABLE)
		require -- from COMPARABLE
			other_exists: other /= void
		ensure -- from COMPARABLE
			equal_zero: (Result = 0) = is_equal (other)
			smaller_negative: (Result = - 1) = (Current < other)
			greater_positive: (Result = 1) = (Current > other)

	infix "<" (other: like Current): BOOLEAN
			-- Is the current time before other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then -- from COMPARABLE
			asymmetric: Result implies not (other < Current)

	infix "<=" (other: like Current): BOOLEAN
			-- Is current object less than or equal to other?
			-- (from COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then -- from COMPARABLE
			definition: Result = ((Current < other) or is_equal (other))

	infix ">" (other: like Current): BOOLEAN
			-- Is current object greater than other?
			-- (from COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then -- from COMPARABLE
			definition: Result = (other < Current)

	infix ">=" (other: like Current): BOOLEAN
			-- Is current object greater than or equal to other?
			-- (from COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then -- from COMPARABLE
			definition: Result = (other <= Current)
	
feature -- Element change

	set_fine_second (s: DOUBLE)
			-- Set fine_second to s
			-- (from TIME_VALUE)
		require -- from TIME_MEASUREMENT
			s_large_enough: s >= 0
			s_small_enough: s < seconds_in_minute
		ensure -- from TIME_MEASUREMENT
			fine_second_set: fine_second = s

	set_fractionals (f: DOUBLE)
			-- Set fractional_second to f.
			-- (from TIME_VALUE)
		require -- from TIME_MEASUREMENT
			f_large_enough: f >= 0
			f_small_enough: f < 1
		ensure -- from TIME_MEASUREMENT
			second_same: second = old second

	set_hour (h: INTEGER)
			-- Set hour to h.
			-- (from TIME_VALUE)
		require -- from TIME_MEASUREMENT
			h_large_enough: h >= 0
			h_small_enough: h < hours_in_day
		ensure -- from TIME_MEASUREMENT
			hour_set: hour = h

	set_minute (m: INTEGER)
			-- Set minute to m.
			-- (from TIME_VALUE)
		require -- from TIME_MEASUREMENT
			m_large_enough: m >= 0
			m_small_enough: m < minutes_in_hour
		ensure -- from TIME_MEASUREMENT
			minute_set: minute = m

	set_second (s: INTEGER)
			-- Set second to s.
			-- (from TIME_VALUE)
		require -- from TIME_MEASUREMENT
			s_large_enough: s >= 0
			s_small_enough: s < seconds_in_minute
		ensure -- from TIME_MEASUREMENT
			second_set: second = s
	
feature -- Basic operations

	fine_second_add (f: DOUBLE)
			-- Add f seconds to the current time.
			-- if f has decimals, fractional_second is modified.

	hour_add (h: INTEGER)
			-- Add h hours to the current object.

	hour_back
			-- Move to evious hour.

	hour_forth
			-- Move to next hour.

	minute_add (m: INTEGER)
			-- Add m minutes to the current object.

	minute_back
			-- Move to evious minute.

	minute_forth
			-- Move to next minute.

	relative_duration (other: like Current): TIME_DURATION
			-- Duration elapsed from other to Current
		require -- from ABSOLUTE
			other_exists: other /= void
		ensure -- from ABSOLUTE
			result_exists: Result /= void

	second_add (s: INTEGER)
			-- Add s seconds to the current time.

	second_back
			-- Move to previous second.

	second_forth
			-- Move to next second.

	infix "+" (t: TIME_DURATION): TIME
			-- Sum of the current time and duration t
		require
			t_exists: t /= void
		ensure
			result_exists: Result /= void

	infix "-" (other: like Current): INTERVAL [like Current]
			-- Interval between current object and other
			-- (from ABSOLUTE)
		require -- from ABSOLUTE
			other_exists: other /= void
			other_smaller_than_current: other <= Current
		ensure -- from ABSOLUTE
			result_exists: Result /= void
			result_set: Result.start_bound.is_equal (other) and then Result.end_bound.is_equal (Current)
	
feature -- Output

	formatted_out (s: STRING): STRING
			-- Printable representation of time with "standard"
			-- Form: s
		require
			s_exists: s /= void

	out: STRING
			-- Printable representation of time with "standard"
			-- Form: time_default_format_string
	
feature -- Preconditions

	compact_time_valid (c_t: INTEGER): BOOLEAN
			-- Is compact time c_t valid?
			-- (from TIME_VALIDITY_CHECKER)
		require -- from TIME_VALIDITY_CHECKER
			c_t_not_void: c_t /= void

	is_correct_time (h, m: INTEGER; s: DOUBLE; twelve_hour_scale: BOOLEAN): BOOLEAN
			-- Is time represented by h, m, code, and s correct?
			-- twelve_hour_scale specifies if the hour range is 1 - 12
			-- (if True) or 0 - 23 (if False).
			-- (from TIME_VALIDITY_CHECKER)

	time_valid (s: STRING; code_string: STRING): BOOLEAN
			-- Is the code_string enough precise
			-- to create an instance of type TIME?
			-- And does the string s correspond to code_string?
			-- (from TIME_VALIDITY_CHECKER)
		require -- from TIME_VALIDITY_CHECKER
			s_exists: s /= void
			code_exists: code_string /= void
	
invariant

	second_large_enough: second >= 0
	second_small_enough: second < seconds_in_minute
	fractionals_large_enough: fractional_second >= 0
	fractionals_small_enough: fractional_second < 1
	minute_large_enough: minute >= 0
	minute_small_enough: minute < minutes_in_hour
	hour_large_enough: hour >= 0
	hour_small_enough: hour < hours_in_day
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from COMPARABLE
	irreflexive_comparison: not (Current < Current)

end -- class TIME