class interface RECTANGLE

creation
   make
      --  Create default.


   make_points (one: POINT; two: POINT)
      --  Initialise rectangle from two points.

      require
         valid_points: one /= Void and then two /= 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_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 RECTANGLE
   --  General

   out: STRING
      --  Create a new string containing terse printable 
      --  representation of current object.


feature(s) from RECTANGLE
   --  Public rectangle coordinates

   width: INTEGER
      --  Rectangle width


   height: INTEGER
      --  Rectangle height


feature(s) from RECTANGLE
   --  Points making the rectangle

   lower: POINT
      --  Lower point (coordinates < upper).

      ensure
         is_copy:  --  can be modified

   upper: POINT
      --  Upper point.

      ensure
         is_copy:  --  can be modified

feature(s) from RECTANGLE
   --  Changing coordinates

   set_lower (newl: POINT)
      --  Change lower point.

      require
         valid_point: newl /= Void;
         lower: newl.x <= upper.x and newl.y <= upper.y

   set_upper (newu: POINT)
      --  Change upper point.

      require
         valid_point: newu /= Void;
         upper: newu.x >= lower.x and newu.y >= lower.y

   set_width (nwidth: INTEGER)
      --  Change rectangle width.

      require
         positive_size: nwidth >= 0
      ensure
         done: width = nwidth; --  lower constant
         lower: 

   set_height (nheight: INTEGER)
      --  Change rectangle height.

      require
         positive_size: nheight >= 0
      ensure
         done: height = nheight; --  lower constant 
         lower: 

   set_points (one: POINT; two: POINT)
      --  Initialise rectangle from two points.

      require
         valid_points: one /= Void and then two /= Void

   make_points (one: POINT; two: POINT)
      --  Initialise rectangle from two points.

      require
         valid_points: one /= Void and then two /= Void

feature(s) from RECTANGLE
   --  Helper functions

   set_lower_x (xc: INTEGER)
      require
         ok: xc <= upper.x

   set_lower_y (yc: INTEGER)
      require
         ok: yc <= upper.y

   set_upper_x (xc: INTEGER)
      require
         ok: xc >= lower.x

   set_upper_y (yc: INTEGER)
      require
         ok: yc >= lower.y

feature(s) from RECTANGLE
   --  Actions 

   translate_lower (pt: POINT)
      --  Translate rectangle so that lower point is equal to pt
      --  Rectangle size is unchanged. 

      require
         valid_point: pt /= Void
      ensure
         done: lower.is_equal(pt);
         size_unchanged: width = old width and height = old height

   translate_center (pt: POINT)
      --  Translate rectangle so that its center is equal to pt.

      require
         valid_point: pt /= Void
      ensure
         done: center.is_equal(pt);
         size_unchanged: width = old width and height = old height

   translate_upper (pt: POINT)
      --  Translate rectangle so that upper point it pt.

      require
         valid: pt /= Void
      ensure
         done: upper.is_equal(pt);
         size_unchanged: width = old width and height = old height

feature(s) from RECTANGLE
   --  Update

   add (other: RECTANGLE)
      --  Union of rectangles.
      --  Current := (Current) U (other)

      require
         ok: other /= Void

feature(s) from RECTANGLE
   --  Queries

   center: POINT
      --  Return the rectangle centre point.

      ensure
         is_copy:  --  can be modified

   is_point: BOOLEAN
      --  Is the rectangle reduced to a point?


   is_line: BOOLEAN
      --  Is the rectangle reduced to a line (but not a point)?

      ensure
         line_not_point: Result implies not is_point

   is_thin: BOOLEAN
      --  Is the rectangle a line or a point?

      ensure
         done: Result = (is_line or is_point)

   has_point (other: POINT): BOOLEAN
      --  Is point inside current? (not strict)

      require
         valid_point: other /= Void

   is_inside (other: RECTANGLE): BOOLEAN
      --  Is current inside other? (not strict)

      require
         valid_rectangle: other /= Void

invariant
   positive_offset: width > 0 and height > 0;
   coherent_coord: upper.x = lower.x + width - 1 and upper.y = lower.y + height - 1;

end of RECTANGLE