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