class interface P_DATE_TIME creation make 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 P_DATE_TIME -- Creation make feature(s) from P_DATE_TIME -- 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_TIME date: P_DATE -- Gregorian date time: P_TIME -- Time set_date (yyyy, mm, dd: INTEGER) -- Set date. require valid: -- see DATE.set ensure done: date.is_valid set_time (hh, mm, ss: INTEGER) require valid: -- see TIME.set set (yyyy, mo, dd: INTEGER; hh, mi, ss: INTEGER) require valid: -- see DATE.set and TIME.set ensure done: date.is_valid feature(s) from P_DATE_TIME -- Status is_valid: BOOLEAN -- Is the current object holding valid date & time? is_local: BOOLEAN -- Do this date and time have NO timezone information attached? feature(s) from P_DATE_TIME -- Timezone is_utc: BOOLEAN -- Is the current time zone UTC (GMT)? require has_tz: not is_local ensure done: Result = true = timezone_bias = 0 timezone_bias: INTEGER require has_tz: not is_local set_timezone_bias (bias: INTEGER) -- Timezone bias used to convert from the current time to GMT in -- minutes. require bounds: bias < 1440 and bias > - 1440 ensure not_local: not is_local feature(s) from P_DATE_TIME -- Output to_iso: STRING -- Output date and time in ISO 8601 format. feature(s) from P_DATE_TIME -- Output out: STRING -- Output date and time in ISO 8601 format. to_iso_long: STRING -- Output date in ISO verbose format. to_rfc: STRING -- Output date & time in RFC format. invariant valid_date: date /= Void; valid_time: time /= Void; end of P_DATE_TIME