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

class interface
	DATE

create 

	make (y, m, d: INTEGER)
			-- Set year, month and day to y, m, d respectively.
		require
			correct_date: is_correct_date (y, m, d)
		ensure
			year_set: year = y
			month_set: month = m
			day_set: day = d

	make_month_day_year (m, d, y: INTEGER)
			-- Set month, day and year to m, d and y respectively.
		require
			correct_date: is_correct_date (y, m, d)
		ensure
			year_set: year = y
			month_set: month = m
			day_set: day = d

	make_day_month_year (d, m, y: INTEGER)
			-- Set day, month and year to d, m and y respectively.
		require
			correct_date: is_correct_date (y, m, d)
		ensure
			year_set: year = y
			month_set: month = m
			day_set: day = d

	make_now
			-- Set the current object to today's date.

	make_by_days (n: INTEGER)
			-- Set the current date with the number of days n since origin.
		ensure
			days_set: days = n

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

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

	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_valid: date_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_valid: date_valid_with_base (s, code, base)

	make_by_compact_date (c_d: INTEGER)
			-- Initialize from a compact_date.
		require
			c_d_not_void: c_d /= void
			c_d_valid: compact_date_valid (c_d)
		ensure
			compact_date_set: compact_date = c_d

feature -- Access

	compact_date: INTEGER
			-- Day, month and year coded.
			-- (from DATE_VALUE)

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

	day: INTEGER
			-- Day of the current object
			-- (from DATE_VALUE)

	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)

	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)

	month: INTEGER
			-- Month of the current object
			-- (from DATE_VALUE)

	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
			-- Origin date
		ensure -- from ABSOLUTE
			result_exists: Result /= void

	year: INTEGER
			-- Year of the current object
			-- (from DATE_VALUE)
	
feature -- Measurement

	days: INTEGER
			-- Number of days elapsed since origin
		ensure
			same_duration: Result = duration.day

	duration: DATE_DURATION
			-- Definite duration elapsed since origin
		ensure then
			definite_result: Result.definite
			duration_set: ((Current - origin).duration).is_equal (Result)
	
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 date 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

	day_of_january_1st: INTEGER
			-- Day of the week of january 1st of the current year
		ensure
			day_of_the_week_definition: Result > 0 and then Result < 8

	day_of_the_week: INTEGER
			-- Number of day from the beginning of the week
			-- sunday is 1, etc.., saturday is 7
		ensure
			day_of_the_week_range: Result > 0 and then Result < 8

	days_at_month: INTEGER
			-- Number of days from the beginning of the year
			-- until the beginning of the current month
		ensure
			positive_result: Result >= 0

	days_from (y: INTEGER): INTEGER
			-- Days between the current year and year y

	days_in_year: INTEGER
			-- Number of days in the current year
		ensure
			valid_result: (leap_year implies Result = days_in_leap_year) and then (not leap_year implies Result = days_in_non_leap_year)

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

	leap_year: BOOLEAN
			-- Is the current year a leap year?

	week_of_year: INTEGER
			-- Number of weeks from the beginning of the year
			-- The first week of the year begins on the first sunday of the year
			-- The week number before the first sunday of the year is 0
		ensure
			positive_result: Result >= 0
			result_small_enough: Result < max_weeks_in_year

	year_day: INTEGER
			-- Number of days from the beginning of the year
		ensure
			result_large_enough: Result >= 1
			result_small_enough: Result <= days_in_year
	
feature -- Element change

	set_day (d: INTEGER)
			-- Set day to d.
			-- (from DATE_VALUE)
		require -- from DATE_MEASUREMENT
			d_large_enough: d >= 1
			d_small_enough: d <= days_in_month
		ensure -- from DATE_MEASUREMENT
			day_set: day = d

	set_month (m: INTEGER)
			-- Set month to m.
			-- (from DATE_VALUE)
		require -- from DATE_MEASUREMENT
			m_large_enough: m >= 1
			m_small_enough: m <= months_in_year
			d_small_enough: day <= days_in_i_th_month (m, year)
		ensure -- from DATE_MEASUREMENT
			month_set: month = m

	set_year (y: INTEGER)
			-- Set year to y.
			-- (from DATE_VALUE)
		require -- from DATE_MEASUREMENT
			can_not_cut_29th_feb: day <= days_in_i_th_month (month, y)
		ensure -- from DATE_MEASUREMENT
			year_set: year = y
	
feature -- Conversion

	to_date_time: DATE_TIME
			-- Date-time version, with a zero time component
	
feature -- Basic operations

	add (d: DATE_DURATION)
			-- Adds d to the current date.
			-- if d is not definite, add years and months and then days.

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

	day_back
			-- Move to previous day.
		ensure
			days_set: days = old days - 1

	day_forth
			-- Move to next day.
			-- days is from the origin, day is current.
		ensure
			days_set: days = old days + 1

	month_add (m: INTEGER)
			-- Add m months to the current date.
			-- Can move days backward.

	month_back
			-- Move to previous month.
			-- Can move days backward if previous month has less days than the
			-- current month.

	month_forth
			-- Move to next month.
			-- Can move days backward if next month has less days than the
			-- current month.

	relative_duration (other: like Current): DATE_DURATION
			-- Duration from other to the current date
		require -- from ABSOLUTE
			other_exists: other /= void
		ensure -- from ABSOLUTE
			result_exists: Result /= void
		ensure then
			exact_duration: (other + Result).is_equal (Current)
			canonical_duration: Result.canonical (other)
			origin_date_set: equal (Result.origin_date, other)

	year_add (y: INTEGER)
			-- Add y years to the current date.
			-- May cut the 29th february.
		ensure
			year_set: year = old year + y

	year_back
			-- Move to previous year.
			-- May cut the 29th february.
		ensure
			year_decreased: year = old year - 1

	year_forth
			-- Move to next year.
			-- May cut the 29th february.
		ensure
			year_increased: year = old year + 1

	year_month_add (y, m: INTEGER)
			-- Add y years and m months to the current date.
			-- Check the number of days after.

	infix "+" (d: DATE_DURATION): DATE
			-- Sum to current date the duration d
			-- if duration not define, add years and then months and then days.
		ensure
			result_exists: Result /= void
			definite_set: d.definite implies (Result - Current).duration.is_equal (d)

	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 Current with "standard"
			-- Form: s
		require
			s_exists: s /= void

	out: STRING
			-- Printable representation of Current with "standard"
			-- Form: date_default_format_string
	
feature -- Preconditions

	compact_date_valid (c_d: INTEGER): BOOLEAN
			-- Is compact date c_d valid?
			-- (from DATE_VALIDITY_CHECKER)

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

	date_valid_default (s: STRING): BOOLEAN
			-- Is the code_string enough precise
			-- To create an instance of type DATE
			-- And does the string s correspond to
			-- date_default_format_string?
			-- (from DATE_VALIDITY_CHECKER)
		require -- from DATE_VALIDITY_CHECKER
			s_exists: s /= void

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

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

	is_correct_date (y, m, d: INTEGER): BOOLEAN
			-- Is date specified by y, m, and d a correct date?
			-- (from DATE_VALIDITY_CHECKER)
	
feature -- Status Report

	days_in_month: INTEGER
			-- Number of days in month 'month'.
			-- (from DATE_MEASUREMENT)
		ensure -- from DATE_MEASUREMENT
			positive_result: Result > 0
	
invariant

	day_large_enough: day >= 1
	day_small_enough: day <= days_in_month
	month_large_enough: month >= 1
	month_small_enough: month <= months_in_year
	year_small_enough: year <= 65535
	year_positive: year > 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from COMPARABLE
	irreflexive_comparison: not (Current < Current)

end -- class DATE