note description: "Durations of date" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2017-03-29 12:26:46 +0000 (Wed, 29 Mar 2017) $" revision: "$Revision: 100065 $" access: date class interface DATE_DURATION create make, make_by_days feature -- Initialization make (y, m, d: INTEGER_32) -- Set year, month and day to y, m and d respectively. ensure year_set: year = y month_set: month = m day_set: day = d make_by_days (d: INTEGER_32) -- Set day to d. -- The duration is definite ensure day_set: day = d definite_duration: definite feature -- Access zero: like Current -- Neutral element for "+" and "-" ensure then definite: Result.definite feature -- Attribute day: INTEGER_32 -- Number of days associated with current object month: INTEGER_32 -- Number of monthes associated with current object year: INTEGER_32 -- Number of years associated with current object origin_date: detachable DATE -- Origin date of duration days_count: INTEGER_32 -- Number of days in duration require origin_date_set: has_origin_date feature -- Comparison is_less alias "<" (other: like Current): BOOLEAN -- Is the current object smaller than other? -- It is impossible to compare not definite duration. ensure then definite_duration: (definite and then other.definite) implies Result = (day < other.day) non_definite_duration: (not definite or else not other.definite) implies not Result is_equal (other: like Current): BOOLEAN -- Are the current object and other equal? ensure then result_definition: Result = (year = other.year and then month = other.month and then day = other.day) feature -- Status report definite: BOOLEAN -- Is the duration is independent of the date -- on which it applies? (use of day only)? -- or not (use of year, month and day)? ensure result_definition: Result = ((year = 0) and then (month = 0)) canonical (date: DATE): BOOLEAN -- Is duration expressed minimally for adding to date, i.e. -- If addition will yield a date after date, then: -- year positive, -- month between 0 and Months_in_year - 1, -- day between 0 and (number of days of the month before -- the yielded) - 1? -- If addition will yield a date before date, then: -- year negative, -- month between 1 - Months_in_year and 0, -- day between (number of days of the month before the -- yielded) and 0? require date_exist: date /= Void is_positive: BOOLEAN -- Is duration positive? has_origin_date: BOOLEAN -- Has origin date been set? feature -- Status setting set_origin_date (d: detachable DATE) -- Set origin_date to d. ensure origin_date_set: origin_date = d feature -- Element Change set_day (d: INTEGER_32) -- Set day to d. set_month (m: INTEGER_32) -- Set month to m. set_year (y: INTEGER_32) -- Set year to y. set_date (y, m, d: INTEGER_32) -- Set year with y, month with m and day with d. day_add (d: INTEGER_32) -- Add d days to Current. ensure day_set: day = old day + d month_add (m: INTEGER_32) -- Add m months to Current. ensure month_set: month = old month + m year_add (y: INTEGER_32) -- Add y years to Current. ensure year_set: year = old year + y feature -- Basic operations plus alias "+" (other: like Current): like Current -- Sum of current object with other ensure then origin_equal: equal (origin_date, Result.origin_date) opposite alias "-": like Current -- Unary minus ensure then origin_equal: equal (origin_date, Result.origin_date) feature -- Conversion to_canonical (start_date: DATE): like Current -- A new duration, equivalent to current one -- and canonical for date require start_date_not_void: start_date /= Void ensure canonical_result: Result.canonical (start_date) duration_not_changed: equal (start_date + Current, start_date + Result) to_definite (date: DATE) -- Make current duration definite. require date_exists: date /= Void ensure definite_result: definite to_date_time: DATE_TIME_DURATION -- Date-time version, with a zero time component ensure result_exists: Result /= Void year_set: Result.year = year month_set: Result.month = month day_set: Result.day = day invariant equal_signs: (has_origin_date and then attached origin_date as l_origin_date and then canonical (l_origin_date)) implies (day >= 0 and month >= 0 and year >= 0) or (day <= 0 and month <= 0 and year <= 0) note copyright: "Copyright (c) 1984-2017, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class DATE_DURATION
Generated by ISE EiffelStudio