82 lines
1.6 KiB
Plaintext
82 lines
1.6 KiB
Plaintext
class
|
|
CIRCLE
|
|
|
|
inherit
|
|
POINT
|
|
rename
|
|
make as point_make
|
|
redefine
|
|
make_origin,
|
|
out
|
|
end
|
|
create
|
|
make, make_origin, make_from_point
|
|
|
|
feature -- Initialization
|
|
|
|
make (a_x, a_y, a_r: INTEGER)
|
|
-- Create with values `a_x' and `a_y' and `a_r'
|
|
require
|
|
non_negative_radius_argument: a_r >= 0
|
|
do
|
|
point_make (a_x, a_y)
|
|
set_r (a_r)
|
|
ensure
|
|
x_set: x = a_x
|
|
y_set: y = a_y
|
|
r_set: r = a_r
|
|
end
|
|
|
|
make_origin
|
|
-- Create at origin with zero radius
|
|
do
|
|
Precursor
|
|
ensure then
|
|
r_set: r = 0
|
|
end
|
|
|
|
make_from_point (a_p: POINT; a_r: INTEGER)
|
|
-- Initialize from `a_r' with radius `a_r'.
|
|
require
|
|
non_negative_radius_argument: a_r >= 0
|
|
do
|
|
set_x (a_p.x)
|
|
set_y (a_p.y)
|
|
set_r (a_r)
|
|
ensure
|
|
x_set: x = a_p.x
|
|
y_set: y = a_p.y
|
|
r_set: r = a_r
|
|
end
|
|
|
|
feature -- Access
|
|
|
|
r: INTEGER assign set_r
|
|
-- Radius
|
|
|
|
feature -- Element change
|
|
|
|
set_r (a_r: INTEGER)
|
|
-- Set radius (`r') to `a_r'
|
|
require
|
|
non_negative_radius_argument: a_r >= 0
|
|
do
|
|
r := a_r
|
|
ensure
|
|
r_set: r = a_r
|
|
end
|
|
|
|
feature -- Output
|
|
|
|
out: STRING
|
|
-- Display as string
|
|
do
|
|
Result := "Circle: x = " + x.out + " y = " + y.out + " r = " + r.out
|
|
end
|
|
|
|
invariant
|
|
|
|
non_negative_radius: r >= 0
|
|
|
|
end
|