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

class interface
	DATE_VALUE

feature -- Access

	compact_date: INTEGER
			-- Day, month and year coded.

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

	day: INTEGER
			-- Day of the current object

	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

	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)

	year: INTEGER
			-- Year of the current object
	
feature -- Status report

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

	set_day (d: INTEGER)
			-- Set day to d.
		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.
		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.
		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 -- Status Report

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

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class DATE_VALUE