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

class interface
	TIME_DURATION

create 

	make (h, m, s: INTEGER)
			-- Set hour, minute and second to h, m, s respectively.
		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.
		ensure
			hour_set: hour = h
			minute_set: minute = m
			fine_second_set: fine_second = s

	make_by_seconds (s: INTEGER)
			-- Set the object by the number of seconds s.
		ensure
			seconds_count_set: seconds_count = s

	make_by_fine_seconds (s: DOUBLE)
			-- Set the object by the number of seconds s.
		ensure
			minute_large_enough: minute >= 0
			minute_small_enough: minute < minutes_in_hour
			second_large_enough: second >= 0
			second_small_enough: second < seconds_in_minute
			fine_seconds_set: dabs (fine_seconds_count - s) <= tolerance

feature -- Initialization

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

	make_by_fine_seconds (s: DOUBLE)
			-- Set the object by the number of seconds s.
		ensure
			minute_large_enough: minute >= 0
			minute_small_enough: minute < minutes_in_hour
			second_large_enough: second >= 0
			second_small_enough: second < seconds_in_minute
			fine_seconds_set: dabs (fine_seconds_count - s) <= tolerance

	make_by_seconds (s: INTEGER)
			-- Set the object by the number of seconds s.
		ensure
			seconds_count_set: seconds_count = 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.
		ensure
			hour_set: hour = h
			minute_set: minute = m
			fine_second_set: fine_second = s
	
feature -- Access

	fine_seconds_count: DOUBLE
			-- Number of seconds and fractionals of seconds of current duration

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

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

	seconds_count: INTEGER
			-- Total number of seconds of current duration
		ensure
			same_count: Result = fine_seconds_count.truncated_to_integer

	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)

	zero: TIME_DURATION
			-- Neutral element for "+" and "-"
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
	
feature -- Comparison

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

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

	infix ">=" (other: like Current): BOOLEAN
			-- Is current object greater than or equal to other?
			-- (from PART_COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void
	
feature -- Status report

	canonical: BOOLEAN
			-- Is duration expressed minimally, i.e.
			--	If duration is positive then
			--		hour positive,
			--		minute and second between 0 and 59,
			--		fractional_second between 0 and 999?
			--	If duration is negative then
			--		hour negative,
			--		minute and second between -59 and 0,
			--		fractional_second between -999 and 0?

	is_negative: BOOLEAN
			-- Is duration negative?
			-- (from DURATION)

	is_positive: BOOLEAN
			-- Is duration positive?

	is_zero: BOOLEAN
			-- Is duration zero?
			-- (from DURATION)
	
feature -- Element change

	prefix "+": like Current
			-- Unary plus
			-- (from DURATION)
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			result_definition: Result.is_equal (Current)

	infix "-" (other: like Current): like Current
			-- Difference with other
			-- (from DURATION)
		require -- from GROUP_ELEMENT
			other_exists: other /= void
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
	
feature -- Conversion

	time_modulo_day: like Current
			-- Duration modulo duration of a day
		ensure
			result_smaller_than_day: Result.seconds_count < seconds_in_day
			result_positive: Result >= zero

	to_canonical: like Current
			-- A new duration
		ensure
			result_canonical: Result.canonical

	to_days: INTEGER
			-- Total number of days equivalent to the current duration
	
feature -- Basic operations

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

	hour_add (h: INTEGER)
			-- Add h hours to the current duration.
		ensure
			hour_set: hour = old hour + h

	minute_add (m: INTEGER)
			-- Add m minutes to the current duration.
		ensure
			minute_set: minute = old minute + m

	second_add (s: INTEGER)
			-- Add s seconds to the current duration.
		ensure
			second_set: second = old second + s

	infix "+" (other: like Current): like Current
			-- Sum with other
		require -- from GROUP_ELEMENT
			other_exists: other /= void
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			commutative: Result.is_equal (other + Current)

	prefix "-": like Current
			-- Unary minus
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			result_definition: (Result + Current).is_equal (zero)
	
feature -- Attributes

	fine_second: DOUBLE

	fractional_second: DOUBLE

	hour: INTEGER

	minute: INTEGER

	second: INTEGER
	
feature -- Comparaison

	is_equal (other: like Current): BOOLEAN
			-- Is the current duration equal to other?
		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

	infix "<" (other: like Current): BOOLEAN
			-- Is the current duration smaller than other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
	
feature -- Element Change

	set_fine_second (s: DOUBLE)
			-- Set fine_second to s.
		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.
			-- f must have the same sign as second.
		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.
		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.
		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.
			-- fractional_second is cut down to 0.
		require -- from TIME_MEASUREMENT
			s_large_enough: s >= 0
			s_small_enough: s < seconds_in_minute
		ensure -- from TIME_MEASUREMENT
			second_set: second = s
	
invariant

	fractionals_large_enough: fractional_second > - 1
	fractionals_small_enough: fractional_second < 1
	fractional_and_second_same_sign: second * fractional_second >= 0
	equal_signs: canonical implies (hour >= 0 and minute >= 0 and fine_second >= 0) or (hour <= 0 and minute <= 0 and fine_second <= 0)
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from DURATION
	sign_correctness: is_positive xor is_negative xor is_zero
		-- from GROUP_ELEMENT
	neutral_addition: Current.is_equal (Current + zero)
	self_subtraction: zero.is_equal (Current - Current)

end -- class TIME_DURATION