class interface P_DATE feature(s) from HASHABLE hash_code: INTEGER -- The hash-code value of Current. ensure good_hash_value: Result >= 0 feature(s) from P_TEXT_OBJECT -- Public interface to_string: STRING ensure is_copy: Result /= Void from_string (str: STRING) -- Init object from string. require valid: str /= Void ensure done: -- success implies to_string.is_equal(str) feature(s) from COMPARABLE infix "<" (other: like Current): BOOLEAN -- Is Current strictly less than other? require other_exists: other /= Void ensure asymmetric: Result implies not (other < Current) infix "<=" (other: like Current): BOOLEAN -- Is Current less than or equal other? require other_exists: other /= Void ensure definition: Result = (Current < other or is_equal(other)) infix ">" (other: like Current): BOOLEAN -- Is Current strictly greater than other? require other_exists: other /= Void ensure definition: Result = (other < Current) infix ">=" (other: like Current): BOOLEAN -- Is Current greater than or equal than other? require other_exists: other /= Void ensure definition: Result = (other <= Current) in_range (lower, upper: like Current): BOOLEAN -- Return true if Current is in range [lower..upper] ensure Result = (Current >= lower and Current <= upper) compare (other: like Current): INTEGER -- If current object equal to other, 0; -- if smaller, -1; if greater, 1. require other_exists: other /= Void ensure equal_zero: Result = 0 = is_equal(other); smaller_negative: Result = - 1 = Current < other; greater_positive: Result = 1 = Current > other three_way_comparison (other: like Current): INTEGER -- If current object equal to other, 0; -- if smaller, -1; if greater, 1. require other_exists: other /= Void ensure equal_zero: Result = 0 = is_equal(other); smaller_negative: Result = - 1 = Current < other; greater_positive: Result = 1 = Current > other min (other: like Current): like Current -- Minimum of Current and other. require other /= Void ensure Result <= Current and then Result <= other; compare(Result) = 0 or else other.compare(Result) = 0 max (other: like Current): like Current -- Maximum of Current and other. require other /= Void ensure Result >= Current and then Result >= other; compare(Result) = 0 or else other.compare(Result) = 0 feature(s) from P_DATE -- Comparison is_equal (other: like Current): BOOLEAN -- Is other attached to an object considered equal to -- current object ? require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) feature(s) from P_DATE year: INTEGER -- Full gregorian year. month: INTEGER -- Month (1-12) day: INTEGER -- Day (1-31) day_of_year: INTEGER -- Day of year. require valid: is_valid ensure valid: Result > 0 and Result <= 366 day_of_week: INTEGER -- Day of week (0 = Sunday). require valid: is_valid; modern: year > 1752 -- and not russia < 19xx ... ensure valid: Result >= 0 and Result < 7 feature(s) from P_DATE set_year (yyyy: INTEGER) -- Set year. require positive: yyyy > 0 ensure done: yyyy = year set_month (mm: INTEGER) -- Set month. require valid: mm >= 1 and mm <= 12 ensure done: mm = month set_day (dd: INTEGER) -- Set day. require valid: dd >= 1 and dd <= 31 ensure done: dd = day set (yyyy, mm, dd: INTEGER) -- Set date. require valid_date: is_valid_date(yyyy,mm,dd) ensure done: dd = day and mm = month and yyyy = year; valid: is_valid feature(s) from P_DATE -- Status is_valid_date (yyyy, mm, dd: INTEGER): BOOLEAN -- Is the given date valid. is_valid: BOOLEAN -- Is the current date valid? is_leap_year: BOOLEAN -- Is the current year a leap year? feature(s) from P_DATE -- Output out: STRING -- Create a new string containing terse printable -- representation of current object. to_iso_long: STRING -- Output date in verbose ISO format. -- eg: "1887-07-26" require ok: is_valid ensure is_copy: Result /= Void to_iso: STRING -- Output date in compact ISO format. -- eg: "18870726" require ok: is_valid ensure is_copy: Result /= Void to_rfc: STRING -- Output date in canonical RFC 822 format. -- eg: "26 Jul 1887", in English. require ok: is_valid ensure is_copy: Result /= Void to_european: STRING -- Output date using usual numeric european format. -- eg: "26/07/1887" require ok: is_valid ensure is_copy: Result /= Void to_american: STRING -- Output date using usual numeric american format. -- eg: "07/26/1887" require ok: is_valid ensure is_copy: Result /= Void end of P_DATE