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