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