Category : Files from Magazines
Archive   : DDJ1289.ZIP
Filename : MEYER.LST

 
Output of file : MEYER.LST contained in archive : DDJ1289.ZIP

_WRITING CORRECT SOFTWARE WITH EIFFEL_
by Bertrand Meyer


[LISTING ONE]

class CIRCLE export
center, radius, intersect1, intersect2,
on, inside, outside,
translate, scale, rotate ...
feature
center: POINT;
radius: REAL;

intersect1(other: CIRCLE): POINT is
-- One of the intersections
-- of current circle with other
require
not other.Void;
center.distance(other.center)
<=radius + other.radius
do
... Computation of intersection ...
ensure
on(Result);
other.on(Result);
end; -- intersect1

intersect2(other:CIRCLE): POINT is
...

on(p:POINT) is
-- IS p on circle?
require
not p.Void
do ...
end; -- on

inside(p:POINT) is
-- Is p inside circle?
require
not p.Void
do ...
end; -- inside

outside (p:POINT) is
-- Is p outside circle?
require
not p.Void
do ...
end; -- outside

Create (c:POINT; r:REAL) is
--Create circle with center c
--and radius r
require
not c.Void;
r>=0
do
center:=c; radius :=r
end; -- Create

... Other features (translate, scale, ...) ...

invariant
... See below ...
end -- class CIRCLE



[LISTING TWO]

require
other_not_void:not other.Void;
circles_intersect:
center.distance (other.center)
<=radius + other.radius

[LISTING THREE]

class interface CIRCLE
exported features
center, radius, intersect1, intersect2,
on, inside, outside,
translate, scale, rotate ...
feature specification
center: POINT;
radius: REAL;

intersect1(other: CIRCLE): POINT
-- One of the intersections
-- of current circle with other

require
not other.Void;
center.distance(other.center)
<=radius + other.radius
ensure
on(Result)
other.on(Result)

intersect(other:CIRCLE): POINT
...

on(p:POINT)
-- Is p on circle?
require
not p.Void

inside(p:POINT)
-- Is p inside circle?
require
not p.Void
ensure
Result=(center.distance(p)
outside(p:POINT)
...

...Specification of other features
(translate, scale, ...) ...

invariant
... See below ...

end -- class interface CIRCLE




[LISTING FOUR]

r is
require
p
do
if not p then
... Deal with erroneous case ...
else
... Proceed with normal execution ...
end
end; -- p




[LISTING FIVE]

class C [T] export
write, write_successful,...
feature

write_successful: BOOLEAN;
-- An attribute

write (x: T) is
-- Write x, if possible;
-- make at most five attempts.
-- Record result in write_successful
local
attempts: INTEGER
external
attempt_to_write (x:T)
language "..."
do
if attempts <5 then
attempt_to_write (x);
write_successful:=true
else
write_successful:=false
end
rescue
attempts:=attempts+1;
retry
end -- write
...
end -- class C



[LISTING SIX]

write(x: T) is
-- Write x;
-- make at most five attempts.
local
attempts:INTEGER
external
... As before ...

do
attempts:=attempts+1;
attempt_to_write(x);
rescue
if attempts < 5 then
retry
end
end -- write