class interface DRAWABLE_ROUND_RECTANGLE
creation
make
-- Creation.
feature(s) from DRAWABLE_RECTANGLE
-- Position
set_position (rect: RECTANGLE)
-- Set rectangle to be drawn.
require
valid_rectangle: rect /= Void
ensure
done: position.is_equal(rect)
feature(s) from DRAWABLE_ROUND_RECTANGLE
-- Position
set_corner (width, height: INTEGER)
-- Set the width and height of the ellipse used to draw the
-- rounded corners of the rectangle.
ensure
done: round_width = width and then round_height = height
invariant
valid_position: position /= Void;
end of DRAWABLE_ROUND_RECTANGLE