Simtel MSDOS 1992 September/Simtel20_Sept92.cdr/msdos/ddjmag/ddj8912.arc/MEYER.LST

File List | 1989-10-30 | 5KB | 202 lines

_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)<radius)

      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