Abstract
To show that a computer graphics system functions properly it is necessary to prove that the images it produces are correct. Most graphical devices are unable to exactly represent an image, or even just a straight line. Thus each device must display an approximation to the ideal. This paper presents a formal specification of the properties any reasonable approximation to a straight line should have. Bresenham's algorithm is shown to satisfy this specification and extensions to the specification are discussed.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. Arcelli and A. Massarotti, "Regular Arcs in Digital Contours," Computer Graphics and Image Processing Vol. 4 pp. 339–360 (1975).
G. Bongiovanni, F. Luccio, and A. Zorat, "The Discrete Equation of a Straight Line," IEEE Transactions on Computers Vol. C-24(3) pp. 310–313 (March 1975).
J. Boothroyd and P. A. Hamilton, "Exactly Reversible Plotter Paths," Australian Computer Journal Vol. 2(1) pp. 20–21 (1970).
J. E. Bresenham, "Algorithm for Computer Control of a Digital Plotter," IBM Systems Journal Vol. 4(1) pp. 25–30 (1965).
K. W. Brodlie, M. C. Maguire, and G. E. Pfaff, "A Practical Strategy for Certifying GKS Implementations," in EUROGRAPHICS 82 International Conference and Exhibition UMIST 8–10 Sept 1982, eds. D. S. Greenaway and E. A. Warman, North-Holland (1982).
R. Brons, "Linguistic Methods for the Description of a Straight Line on a Grid," Computer Graphics and Image Processing Vol. 3 pp. 48–62 (1974).
George S. Carson, "The Specification of Computer Graphics Systems," IEEE Computer Graphics and Applications Vol. 3(6) pp. 27–41 (1974).
D. A. Duce, E. V. C. Fielding, and L. S. Marshall, Formal Specification and Graphics Software, Rutherford Appleton Laboratory Report RAL-84-068, August 1984.
R. A. Earnshaw, Display Algorithms — History, Developments and Applications, University Computing Service, University of Leeds.
Eugene Fiume and Alain Fournier, A Programme for the Development of a Mathematical Theory of Computer Graphics, Computer Systems Research Group, Department of Computer Science, University of Toronto, Toronto, Ontario (1984).
J. D. Foley and A. van Dam, Fundamentals of Interactive Computer Graphics, Addison-Wesley Publishing Company (1982).
Herbert Freeman, "Boundary Encoding and Processing," pp. 241–266 in Picture Processing and Psychopictorics, eds. Bernice Sacks Lipkin and Azriel Rosenfeld, Academic Press, New York-London (1970).
Graphical Kernel System (GKS) 7.2 Functional Description, Draft International Standard ISO/DIS 7942 (November 14th, 1982).
R. Gnatz, Approaching a Formal Framework for Graphics Software Standards, Technical University of Munich.
Leo J. Guibas and Jorge Stolfi, "A Language for Bitmap Manipulation," ACM Transactions on Graphics Vol. 1(3) pp. 191–214 (July 1982).
Satish Gupta and Robert F. Sproull, "Filtering Edges for Grey-Scale Displays," ACM Computer Graphics Vol. 15(3) pp. 1–5 (August 1981).
John Guttag and James J. Horning, Formal Specification as a Design Tool, XEROX PARC Technical Report CSL-80-1, Palo Alto, CA (June 1982).
C. B. Jones, Software Development: A Rigorous Approach, Prentice-Hall, Englewood Cliffs, NJ (1980).
William R. Mallgren, Formal Specification of Interactive Graphics Programming Languages, ACM Distinguished Dissertation 1982, MIT Press (1983).
Lynn S. Marshall, A Formal Specification of Line Representations on Graphics Devices, University of Manchester Transfer Report, September 1984.
Lynn S. Marshall, GKS Workstations: Formal Specification and Proofs of Correctness for Specific Devices, University of Manchester Transfer Report, September 1984.
William M. Newman and Robert F. Sproull, Principles of Interactive Computer Graphics, McGraw Hill Kogakuska Limited (1973).
William M. Newman and Robert F. Sproull, Principles of Interactive Computer Graphics, Second Edition, McGraw Hill International Book Company (1981).
M. L. V. Pitteway and D. J. Watkinson, "Bresenham's Algorithm with Grey Scale," Communications of the ACM Vol. 23(11) pp. 625–626 (1980).
Azriel Rosenfeld, "Digital Straight Line Segments," IEEE Transactions on Computers Vol. C-23(12) pp. 1264–1269 (December 1974).
Jerome Rothstein and Carl Weiman, "Parallel and Sequential Specification of a Context Sensitive Language for Straight Lines on Grids," Computer Graphics and Image Processing Vol. 5 pp. 106–124 (1976).
Robert F. Sproull, "Using Program Transformations to Derive Line Drawing Algorithms," ACM Transactions on Graphics Vol. 1(4) pp. 259–273 (October 1982).
University of Manchester Computer Graphics Unit, Interactive Computer Graphics Course Notes (March 1984).
John Warnock and Douglas K. Wyatt, "A Device Independent Graphics Imaging Model for Use with Raster Devices," ACM Computer Graphics Vol. 16(3) pp. 313–319 (July 1982).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marshall, L.S. (1985). A formal specification of line representations on graphics devices. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds) Formal Methods and Software Development. TAPSOFT 1985. Lecture Notes in Computer Science, vol 186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15199-0_9
Download citation
DOI: https://doi.org/10.1007/3-540-15199-0_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15199-9
Online ISBN: 978-3-540-39307-8
eBook Packages: Springer Book Archive