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

class interface
	DATE_TIME_VALUE

feature -- Access

	date: DATE_VALUE
			-- Date of the current object

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

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

	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
			-- Decimal part of second
		ensure
			same_fractional: Result = time.fractional_second

	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)

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

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

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

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

	is_leap_year (y: INTEGER): BOOLEAN
			-- Is year y a leap year?
			-- (from DATE_CONSTANTS)
	
invariant

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

end -- class DATE_TIME_VALUE