indexing
	description: "Date Measurement"
	date: "$Date$"
	revision: "$Revision$"

deferred class interface
	DATE_MEASUREMENT

feature -- Access

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

	day: INTEGER
			-- Number of days associated with 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
			-- Number of monthes associated with 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
			-- Number of years associated with 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
			d_large_enough: d >= 1
			d_small_enough: d <= days_in_month
		ensure
			day_set: day = d

	set_month (m: INTEGER)
			-- Set month to m.
			-- day must be small enough.
		require
			m_large_enough: m >= 1
			m_small_enough: m <= months_in_year
			d_small_enough: day <= days_in_i_th_month (m, year)
		ensure
			month_set: month = m

	set_year (y: INTEGER)
			-- Set year to y.
		require
			can_not_cut_29th_feb: day <= days_in_i_th_month (month, y)
		ensure
			year_set: year = y
	
feature -- Status Report

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

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

end -- class DATE_MEASUREMENT