indexing
	description: "Absolute temporal values composed of a date and a time"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"
	access: date, time

class interface
	DATE_TIME

create 

	make (y, mo, d, h, mi, s: INTEGER)
			-- Set year, month day to y, mo, d.
			-- Set hour, minute, second to h, mi, s.
		require
			correct_date_time: is_correct_date_time (y, mo, d, h, mi, s, False)
		ensure
			year_set: year = y
			month_set: month = mo
			day_set: day = d
			hour_set: hour = h
			minute_set: minute = mi
			second_set: second = s

	make_fine (y, mo, d, h, mi: INTEGER; s: DOUBLE)
			-- Set year, month day to y, mo, d.
			-- Set hour, minute, second to h, m, s.
		require
			correct_date_time: is_correct_date_time (y, mo, d, h, mi, s, False)
		ensure
			year_set: year = y
			month_set: month = mo
			day_set: day = d
			hour_set: hour = h
			minute_set: minute = mi
			second_set: fine_second = s

	make_by_date_time (d: DATE; t: TIME)
			-- Set date to d and time to t
		require
			d_exists: d /= void
			t_exists: t /= void
		ensure
			date_set: date = d
			time_set: time = t

	make_by_date (d: DATE)
			-- Set date to d and time to origin of time.
		require
			d_exists: d /= void
		ensure
			date_set: date = d
			time_set: time.is_equal (time.origin)

	make_now
			-- Get the date and the time from the system.

	make_from_string (s: STRING; code: STRING)
			-- Initialize from a "standard" string of form
			-- code.
			-- (For 2-digit year specifications, the current century is used as
			-- base century.)
		require
			s_exists: s /= void
			c_exists: code /= void
			date_time_valid: date_time_valid (s, code)

	make_from_string_with_base (s: STRING; code: STRING; base: INTEGER)
			-- Initialize from a "standard" string of form
			-- code with base century base.
		require
			s_exists: s /= void
			c_exists: code /= void
			base_valid: base > 0 and (base \\ 100 = 0)
			date_time_valid: date_time_valid_with_base (s, code, base)

	make_from_string_default (s: STRING)
			-- Initialize from a "standard" string of form
			-- default_format_string.
			-- (For 2-digit year specifications, the current century is used as
			-- base century.)
		require
			s_exists: s /= void
			date_time_valid: date_time_valid (s, default_format_string)

	make_from_string_default_with_base (s: STRING; base: INTEGER)
			-- Initialize from a "standard" string of form
			-- default_format_string with base century base.
		require
			s_exists: s /= void
			base_valid: base > 0 and (base \\ 100 = 0)
			date_time_valid: date_time_valid_with_base (s, default_format_string, base)

feature -- Initialization

	make (y, mo, d, h, mi, s: INTEGER)
			-- Set year, month day to y, mo, d.
			-- Set hour, minute, second to h, mi, s.
		require
			correct_date_time: is_correct_date_time (y, mo, d, h, mi, s, False)
		ensure
			year_set: year = y
			month_set: month = mo
			day_set: day = d
			hour_set: hour = h
			minute_set: minute = mi
			second_set: second = s

	make_by_date (d: DATE)
			-- Set date to d and time to origin of time.
		require
			d_exists: d /= void
		ensure
			date_set: date = d
			time_set: time.is_equal (time.origin)

	make_by_date_time (d: DATE; t: TIME)
			-- Set date to d and time to t
		require
			d_exists: d /= void
			t_exists: t /= void
		ensure
			date_set: date = d
			time_set: time = t

	make_fine (y, mo, d, h, mi: INTEGER; s: DOUBLE)
			-- Set year, month day to y, mo, d.
			-- Set hour, minute, second to h, m, s.
		require
			correct_date_time: is_correct_date_time (y, mo, d, h, mi, s, False)
		ensure
			year_set: year = y
			month_set: month = mo
			day_set: day = d
			hour_set: hour = h
			minute_set: minute = mi
			second_set: fine_second = s

	make_from_string (s: STRING; code: STRING)
			-- Initialize from a "standard" string of form
			-- code.
			-- (For 2-digit year specifications, the current century is used as
			-- base century.)
		require
			s_exists: s /= void
			c_exists: code /= void
			date_time_valid: date_time_valid (s, code)

	make_from_string_default (s: STRING)
			-- Initialize from a "standard" string of form
			-- default_format_string.
			-- (For 2-digit year specifications, the current century is used as
			-- base century.)
		require
			s_exists: s /= void
			date_time_valid: date_time_valid (s, default_format_string)

	make_from_string_default_with_base (s: STRING; base: INTEGER)
			-- Initialize from a "standard" string of form
			-- default_format_string with base century base.
		require
			s_exists: s /= void
			base_valid: base > 0 and (base \\ 100 = 0)
			date_time_valid: date_time_valid_with_base (s, default_format_string, base)

	make_from_string_with_base (s: STRING; code: STRING; base: INTEGER)
			-- Initialize from a "standard" string of form
			-- code with base century base.
		require
			s_exists: s /= void
			c_exists: code /= void
			base_valid: base > 0 and (base \\ 100 = 0)
			date_time_valid: date_time_valid_with_base (s, code, base)

	make_now
			-- Get the date and the time from the system.
	
feature -- Access

	date: DATE
			-- Date of the current object

	date_default_format_string: STRING
			-- Default output format for dates
			-- (from DATE_CONSTANTS)

	date_duration: DATE_DURATION
			-- Definite duration between origin of date and current date

	day: INTEGER
			-- Day of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_day: Result = date.day

	days: INTEGER
			-- Number of days elapsed since origin

	days_in_i_th_month (i, y: INTEGER): INTEGER
			-- Number of days in the i th month at year y
			-- (from DATE_CONSTANTS)
		require -- from DATE_CONSTANTS
			i_large_enough: i >= 1
			i_small_enough: i <= months_in_year

	Days_in_leap_year: INTEGER is 366
			-- Number of days in a leap year
			-- (from DATE_CONSTANTS)

	Days_in_non_leap_year: INTEGER is 365
			-- Number of days in a non-leap year
			-- (from DATE_CONSTANTS)

	Days_in_week: INTEGER is 7
			-- Number of days in a week
			-- (from DATE_CONSTANTS)

	days_text: ARRAY [STRING]
			-- Short text representation of days
			-- (from DATE_CONSTANTS)

	fine_second: DOUBLE
			-- Representation of second with decimals
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_fine_second: Result = time.fine_second

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

	hour: INTEGER
			-- Hour of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_hour: Result = time.hour

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

	long_days_text: ARRAY [STRING]
			-- Long text representation of days
			-- (from DATE_CONSTANTS)

	long_months_text: ARRAY [STRING]
			-- Long text representation of months
			-- (from DATE_CONSTANTS)

	Max_weeks_in_year: INTEGER is 53
			-- Maximun number of weeks in a year
			-- (from DATE_CONSTANTS)

	minute: INTEGER
			-- Minute of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_minute: Result = time.minute

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

	month: INTEGER
			-- Month of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_month: Result = date.month

	Months_in_year: INTEGER is 12
			-- Number of months in year
			-- (from DATE_CONSTANTS)

	months_text: ARRAY [STRING]
			-- Short text representation of months
			-- (from DATE_CONSTANTS)

	origin: DATE_TIME
			-- Origin date with origin time
		ensure -- from ABSOLUTE
			result_exists: Result /= void

	second: INTEGER
			-- Second of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_second: Result = time.second

	seconds: INTEGER
			-- Number of seconds elapsed from midnight of the current date

	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: TIME
			-- Time of the current object

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

	time_duration: TIME_DURATION
			-- Duration elapsed from midnight of the current date

	year: INTEGER
			-- Year of the current object
			-- (from DATE_TIME_MEASUREMENT)
		ensure -- from DATE_TIME_MEASUREMENT
			same_year: Result = date.year
	
feature -- Measurement

	duration: DATE_TIME_DURATION
			-- Definite duration elapsed from origin
		ensure then
			definite_result: Result.definite
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is the current object 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
		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 object 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 -- Status report

	is_leap_year (y: INTEGER): BOOLEAN
			-- Is year y a leap year?
			-- (from DATE_CONSTANTS)
	
feature -- Basic operations

	add (dtd: DATE_TIME_DURATION)
			-- Adds dtd to current duration

	day_add (d: INTEGER)
			-- Add d days to the current date.
		ensure
			days_set: days = old days + d

	definite_duration (other: like Current): DATE_TIME_DURATION
			-- Duration from other to the current date, converted to a
			-- definite duration
		require
			other_exists: other /= void
		ensure
			definite_result: Result.definite

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

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

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

	relative_duration (other: like Current): DATE_TIME_DURATION
			-- Duration from other to current date
		require -- from ABSOLUTE
			other_exists: other /= void
		ensure -- from ABSOLUTE
			result_exists: Result /= void
		ensure then
			origin_set: equal (other, Result.origin_date_time)

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

	infix "+" (d: DATE_TIME_DURATION): like Current
			-- Sum the current object with d
		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 -- Element Change

	copy (other: like Current)
			-- set date and time with the other attributes.
		require -- from ANY
			other_not_void: other /= void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)

	set_date (d: DATE)
			-- Set date to d.
		require
			d_exists: d /= void
		ensure
			date_set: date = d

	set_time (t: TIME)
			-- Set time to t.
		require
			t_exists: t /= void
		ensure
			time_set: time = t
	
feature -- Output

	formatted_out (s: STRING): STRING
			-- Printable representation of the current object
			-- With "standard" form: s
		require
			s_exists: s /= void

	out: STRING
			-- Printable representation of the current object
			-- With "standard" form: default_format_string
	
feature -- Preconditions

	date_time_valid (s: STRING; code_string: STRING): BOOLEAN
			-- Is the code_string enough precise
			-- To create an instance of type DATE_TIME
			-- And does the string s correspond to code_string?
			-- (from DATE_TIME_VALIDITY_CHECKER)
		require -- from DATE_TIME_VALIDITY_CHECKER
			s_exists: s /= void
			code_exists: code_string /= void

	date_time_valid_with_base (s: STRING; code_string: STRING; base: INTEGER): BOOLEAN
			-- Is the code_string enough precise
			-- To create an instance of type DATE_TIME
			-- And does the string s correspond to code_string?
			-- Use base century base.
			-- (from DATE_TIME_VALIDITY_CHECKER)
		require -- from DATE_TIME_VALIDITY_CHECKER
			s_exists: s /= void
			code_exists: code_string /= void
			base_valid: base > 0 and (base \\ 100 = 0)

	is_correct_date_time (y, mo, d, h, mi: INTEGER; s: DOUBLE; twelve_hour_scale: BOOLEAN): BOOLEAN
			-- Is date-time specified by y, mo, d, h, mi, s
			-- correct?
			-- twelve_hour_scale specifies if the hour range is 1 - 12
			-- (if True) or 0 - 23 (if False).
			-- (from DATE_TIME_VALIDITY_CHECKER)
	
invariant

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from COMPARABLE
	irreflexive_comparison: not (Current < Current)
		-- from DATE_TIME_MEASUREMENT
	date_exists: date /= void
	time_exists: time /= void

end -- class DATE_TIME