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