Abstract
There is currently much interest, both in academia and industry, in the development and application of formal methods for the specification of computer systems. The need for formal specification is first examined, and broad outlines of current approaches are given. The paper then reviews in more detail the application of such techniques to the specification of graphics systems, in particular standards for computer graphics. The paper concludes with a substantial example taken from the author’s own work towards a formal description of the ISO standard for computer graphics programming, the Graphical Kernel System (GKS).
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
D. B. Arnold, D. A. Duce, and G. J. Reynolds, “An Approach to the Formal Specification of Configurable Models of Graphics Systems,” School of Information Systems, University of East Anglia Norwich UK (1987).
H. Barringer, “A Survey of Verification Techniques for Parallel Programs,” in Lecture Notes in Computer Science Volume 191 ,Springer-Verlag (1985).
K. W. Brodlie and G. E. Pfaff, “Report on the EEC Workshop on Graphics Certification,” Com puter Graphics Forum 1(3), pp. 88–90 (1982).
R. M. Ðurstall and J. A. Goguen, “An Informal Introduction to Specifications Using Clear,” in The Correctness Problem in Computer Science ,ed. R. S. Boyer and J. S. Moore, Academic Press (1981).
G. S. Carson and E. Post, “The Formal Specification of a Computer Graphics System,” TR 83-6, GSC Associates (1983).
G. S. Carson, “The Specification of Computer Graphics Systems,” IEEE Computer Graphics and Applications ,pp. 27–41 (September 1983).
B. Cohen, W. T. Harwood, and M. I. Jackson, The Specification of Complex Systems ,Addison-Wesley Publishing Company (1986).
D. Coleman and R. M. Gallimore, “Software Engineering Using Executable Specifications,” Dept of Computation, UMIST(1984).
ANSI X3H3 Computer Graphics Standards Committee, “American National Standard Functional Specification of the Programmer’s Minimal Interface for Graphics,” X3H3/82-15rl, ANSI Document (1982).
D. A. Duce, “The EEC Workshop on Formal Specification of Graphics Software Standards,” Com puter Graphics Forum 1(3), pp. 92–95 (1982).
D. A. Duce, E. V. C. Fielding, and L. S. Marshall, “Formal Specification and Graphics Software,” RAL-84-068, Rutherford Appleton Laboratory, Chilton, Didcot, OXON OX11 OQX, U.K. (1984).
D. A. Duce and E. V. C. Fielding, “Better Understanding through Formal Specification,” Computer Graphics Forum 4(4), pp. 333–348 (1985).
D. A. Duce and E. V. C. Fielding, “Formal Specification -A Comparison of Two Techniques,” RAL-85-051, Rutherford Appleton Laboratory, Chilton, Didcot, OXON 0X11 OQX, U.K. (1985). (To appear in the Computer Journal 1987)
D. A. Duce and E. V. C. Fielding, “Formal Specification -A Simple Example,” ICL Technical Journal ,pp. 96–111 (May 1986).
D. A. Duce and E. V. C. Fielding, “Towards a Formal Specification of the GKS Output Primitives,”in Proceedings of Eurographics 86 ,ed. A. Requicha, North Holland (1986).
R. Eckert, “Specification of Graphics Systems,” in Methodology of Interaction ,ed. R. A. Guedj, P. J. W. ten Hagen, F. R. A. Hopgood, H. Tucker and D. A. Duce, North-Holland Publishing Comany, 1980.
K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer, “Principles of OBJ2,” Proceedings of the 1985 Symposium on Principles of Programming Languages (1985).
N. Gehani and A. D. McGettrick, Software Specification Techniques ,Addison-Wesley Publishing Company (1986).
R. Gnatz, “An Algebraic Approach to the Standardization and the Certification of Graphics Software,” Computer Graphics Forum 2(2/3), pp. 153–166 (1983).
J. Goguen and J. Meseguer, “Rapid Prototyping in the OBJ Executable Specification Language,” ACM Sigsoft Software Engineering Notes 7(5), p. 75 (1982).
GSPC, “Status Report on the Graphics Standards Planning Committee,” Computer Graphics 13(3) (1979).
R. A. Guedj and H. Tucker, Methodology in Computer Graphics ,North-Holland Publishing Company (1979).
J. Guttag and J. J. Homing, “Formal Specification as a Design Tool,” Proceedings of the Seventh Annual ACM Symposium on Principles of Programming Languages ,Las Vegas, Nev., pp. 251–261 (1980).
M. D. Harrison and A. F. Monk, People and Computers: Designing for Usability ,Cambridge University Press (1986).
I. Hayes, Examples of Specification using Mathematics ,Programming Research Group, Oxford (1985).
F. R. A. Hopgood, D. A. Duce, E. V. C. Fielding, K. Robinson, and A. S. Williams, Methodology of Window Management ,Springer-Verlag (1986).
F. R. A. Hopgood, D. A. Duce, J. R. Gallop, and D. C. Sutcliffe, Introduction to the Graphical Ker nel System (GKS) ,Academic Press (1986). (Second Edition)
ISO, “Information processing systems -Computer graphics -Graphical Kernel System (GKS) functional description,” ISO 7942, ISO Central Secretariat (August 1985).
ISO, “Information processing systems -Computer graphics -Graphical Kernel System (GKS) for three dimensions (GKS-3D) functional description,” ISO/DP 8805 (1985).
ISO, “Information processing systems -Computer graphics -Programmer’s Hierarchical Interactive Graphics System functional description,” ISO/DP (1986).
C. B. Jones, Software Development Using VDM ,Prentice-Hall (1986).
P. A. Koparkar and S. P. Mudur, “The Development of Programs for the Processing of Parametric Curves,” Computer Graphics Forum 2(2/3), pp. 135–144 (1983).
N. G. Leveson, “Software Safety: Why, What and How,” Computing Surveys (June 1985).
W. R. Mallgren, “Formal Specification of Graphic Data Types,” ACM Transactions on Program ming Languages and Systems 4(4), pp. 687–710 (October 1982).
W. R. Mallgren, “Formal Specification of Interactive Graphics Programming Languages,” Technical Report 81-09-01, PhD Dissertation (also published by ACM-MIT Press Distinguished Dissertation Series in June 1983), Department of Computer Science, University of Washington, Seattle.
L. S. Marshall, “A Formal Specification of Line Representations on Graphics Devices,” in Lecture Notes in Computer Science Volumne 186 ,Springer-Verlag (1985).
M. Martins and J. N. Oliveira, “Graphics Programming with Archetypes,” in Proceedings of Euro graphics 85 ,ed. C. V. Vandoni, North Holland (1985).
M. Martins and J. N. Oliveira, “On the Specification of Archetype Oriented Graphics Editors,” Universidade do Minho, Braga, Portugal (1986).
A. D. McGettrick, The Definition of Programming Languages ,Cambridge University Press (1980).
A. J. R. G. Milner, “Is Computing an Experimental Science?,” Inaugural Lecture, Laboratory for the Foundations of Theoretical Computer Science, Department of Computer Science, University of Edinburgh (1986).
C. Morgan, The Schema Language ,Programming Research Group, Oxford (1984).
T. Onodera and S. Kawai, “A formalization for the specification and systematic generation of computer graphics systems,” The Visual Computer 2, pp. 112–126 (1986).
F. G. Pagan, Formal Specification of Programming Languages ,Prentice-Hall (1981).
G. J. Reynolds, “A Token Based Graphics System,” Computer Graphics Forum 5(2), pp. 139–146
D. Richter, “Mappings between Product Data Definitions,” in Proceedings of the Eurographics ’86 Conference ,ed. A. A. G. Requicha, North-Holland Publishing Company (1986).
D. S. H. Rosenthal, “A Framework for Specifying GKS,” X3H3/80-63, ANSI Document (1980).
I. H. Sorensen, “A Design of a Display Interface,” Programming Research Group, University of Oxford (1981).
J. E. Stoy, Denotational Semantics ,The MTT Press (1977).
B. Sufrin, “Z Handbook,” FORSITE Project, Programming Research Group, Oxford (1986).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Duce, D.A. (1988). Formal Specification of Graphics Software. In: Earnshaw, R.A. (eds) Theoretical Foundations of Computer Graphics and CAD. NATO ASI Series, vol 40. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-83539-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-83539-1_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-83541-4
Online ISBN: 978-3-642-83539-1
eBook Packages: Springer Book Archive