class interface P_TIME 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 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_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_TIME -- Status hour: INTEGER -- Hour (0-23) minute: INTEGER -- Minute (0-59) second: INTEGER -- Second (0-59) set_hour (hh: INTEGER) -- Set hour. require valid: hh >= 0 and hh < 24 ensure done: hh = hour set_minute (mm: INTEGER) -- Set minute. require valid: mm >= 0 and mm < 60 ensure done: mm = minute set_second (ss: INTEGER) -- Set second. require valid: ss >= 0 and ss < 60 ensure done: ss = second set (hh, mm, ss: INTEGER) -- Set time. require valid_hour: hh >= 0 and hh < 24; valid_minute: mm >= 0 and mm < 60; valid_second: ss >= 0 and ss < 60 ensure done: hour = hh and minute = mm and second = ss feature(s) from P_TIME -- Status hour_12: INTEGER -- Hour in am/pm format. ensure done: Result >= 1 and Result <= 12 is_am: BOOLEAN -- Is morning? is_pm: BOOLEAN -- Is evening? feature(s) from P_TIME -- Output out: STRING -- Default string representation: ISO format. to_iso: STRING -- Output time in ISO format. -- eg: "233000" ensure is_copy: Result /= Void to_rfc: STRING -- Output time in RFC format. -- eg: "23:30:00" ensure is_copy: Result /= Void invariant hour: hour >= 0 and hour < 24; minute: minute >= 0 and minute < 60; second: second >= 0 and second < 60; ampm: is_am xor is_pm; end of P_TIME