note
	description: "Durations of time"
	legal: "See notice at end of class."
	status: "See notice at end of class."
	date: "$Date: 2017-03-29 12:26:46 +0000 (Wed, 29 Mar 2017) $"
	revision: "$Revision: 100065 $"
	access: time

class interface
	TIME_DURATION

create 
	make,
	make_fine,
	make_by_seconds,
	make_by_fine_seconds

feature -- Initialization

	make (h, m, s: INTEGER_32)
			-- 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_32; s: REAL_64)
			-- 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_32)
			-- Set the object by the number of seconds s.
		ensure
			seconds_count_set: seconds_count = s

	make_by_fine_seconds (s: REAL_64)
			-- 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 -- Access

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

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

	zero: like Current
			-- Neutral element for "+" and "-"
	
feature -- Attributes

	hour: INTEGER_32
			-- Number of hours associated with current object

	minute: INTEGER_32
			-- Number of minutes associated with current object

	second: INTEGER_32
			-- Number of seconds associated with current object.

	fine_second: REAL_64
			-- Number of fine seconds associated with current object

	fractional_second: REAL_64
	
feature -- Comparaison

	is_less alias "<" (other: like Current): BOOLEAN
			-- Is the current duration smaller than other?

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

	set_second (s: INTEGER_32)
			-- Set second to s.
			-- fractional_second is cut down to 0.

	set_fine_second (s: REAL_64)
			-- Set fine_second to s.

	set_fractionals (f: REAL_64)
			-- Set fractional_second to f.
			-- f must have the same sign as second.

	set_minute (m: INTEGER_32)
			-- Set minute to m.

	set_hour (h: INTEGER_32)
			-- Set hour to h.
	
feature -- Basic operations

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

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

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

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

	plus alias "+" (other: like Current): like Current
			-- Sum with other

	opposite alias "-": like Current
			-- Unary minus
	
feature -- Conversion

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

	to_days: INTEGER_32
			-- Total number of days equivalent to the current duration

	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
	
invariant
	fractionals_large_enough: fractional_second > -1.to_double
	fractionals_small_enough: fractional_second < 1.to_double
	fractional_and_second_same_sign: second.to_double * fractional_second >= 0.to_double
	equal_signs: canonical implies (hour >= 0 and minute >= 0 and fine_second >= 0.to_double) or (hour <= 0 and minute <= 0 and fine_second <= 0.to_double)

note
	copyright: "Copyright (c) 1984-2017, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
		Eiffel Software
		5949 Hollister Ave., Goleta, CA 93117 USA
		Telephone 805-685-1006, Fax 805-685-6869
		Website http://www.eiffel.com
		Customer support http://support.eiffel.com
	]"

end -- class TIME_DURATION

Generated by ISE EiffelStudio