Skip to main content

Formal Specification of Graphics Software

  • Conference paper

Part of the book series: NATO ASI Series ((NATO ASI F,volume 40))

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.

Unable to display preview. Download preview PDF.

References

  1. 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).

    Google Scholar 

  2. H. Barringer, “A Survey of Verification Techniques for Parallel Programs,” in Lecture Notes in Computer Science Volume 191 ,Springer-Verlag (1985).

    Google Scholar 

  3. 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).

    Article  Google Scholar 

  4. 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).

    Google Scholar 

  5. G. S. Carson and E. Post, “The Formal Specification of a Computer Graphics System,” TR 83-6, GSC Associates (1983).

    Google Scholar 

  6. G. S. Carson, “The Specification of Computer Graphics Systems,” IEEE Computer Graphics and Applications ,pp. 27–41 (September 1983).

    Google Scholar 

  7. B. Cohen, W. T. Harwood, and M. I. Jackson, The Specification of Complex Systems ,Addison-Wesley Publishing Company (1986).

    Google Scholar 

  8. D. Coleman and R. M. Gallimore, “Software Engineering Using Executable Specifications,” Dept of Computation, UMIST(1984).

    Google Scholar 

  9. 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).

    Google Scholar 

  10. D. A. Duce, “The EEC Workshop on Formal Specification of Graphics Software Standards,” Com puter Graphics Forum 1(3), pp. 92–95 (1982).

    Article  Google Scholar 

  11. 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).

    Google Scholar 

  12. D. A. Duce and E. V. C. Fielding, “Better Understanding through Formal Specification,” Computer Graphics Forum 4(4), pp. 333–348 (1985).

    Article  Google Scholar 

  13. 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)

    Google Scholar 

  14. D. A. Duce and E. V. C. Fielding, “Formal Specification -A Simple Example,” ICL Technical Journal ,pp. 96–111 (May 1986).

    Google Scholar 

  15. 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).

    Google Scholar 

  16. 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.

    Google Scholar 

  17. 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).

    Google Scholar 

  18. N. Gehani and A. D. McGettrick, Software Specification Techniques ,Addison-Wesley Publishing Company (1986).

    Google Scholar 

  19. R. Gnatz, “An Algebraic Approach to the Standardization and the Certification of Graphics Software,” Computer Graphics Forum 2(2/3), pp. 153–166 (1983).

    Article  Google Scholar 

  20. J. Goguen and J. Meseguer, “Rapid Prototyping in the OBJ Executable Specification Language,” ACM Sigsoft Software Engineering Notes 7(5), p. 75 (1982).

    Article  Google Scholar 

  21. GSPC, “Status Report on the Graphics Standards Planning Committee,” Computer Graphics 13(3) (1979).

    Google Scholar 

  22. R. A. Guedj and H. Tucker, Methodology in Computer Graphics ,North-Holland Publishing Company (1979).

    Google Scholar 

  23. 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).

    Google Scholar 

  24. M. D. Harrison and A. F. Monk, People and Computers: Designing for Usability ,Cambridge University Press (1986).

    Google Scholar 

  25. I. Hayes, Examples of Specification using Mathematics ,Programming Research Group, Oxford (1985).

    Google Scholar 

  26. F. R. A. Hopgood, D. A. Duce, E. V. C. Fielding, K. Robinson, and A. S. Williams, Methodology of Window Management ,Springer-Verlag (1986).

    Book  Google Scholar 

  27. 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)

    Google Scholar 

  28. ISO, “Information processing systems -Computer graphics -Graphical Kernel System (GKS) functional description,” ISO 7942, ISO Central Secretariat (August 1985).

    Google Scholar 

  29. ISO, “Information processing systems -Computer graphics -Graphical Kernel System (GKS) for three dimensions (GKS-3D) functional description,” ISO/DP 8805 (1985).

    Google Scholar 

  30. ISO, “Information processing systems -Computer graphics -Programmer’s Hierarchical Interactive Graphics System functional description,” ISO/DP (1986).

    Google Scholar 

  31. C. B. Jones, Software Development Using VDM ,Prentice-Hall (1986).

    MATH  Google Scholar 

  32. 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).

    Article  Google Scholar 

  33. N. G. Leveson, “Software Safety: Why, What and How,” Computing Surveys (June 1985).

    Google Scholar 

  34. W. R. Mallgren, “Formal Specification of Graphic Data Types,” ACM Transactions on Program ming Languages and Systems 4(4), pp. 687–710 (October 1982).

    Article  MATH  Google Scholar 

  35. 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.

    MATH  Google Scholar 

  36. L. S. Marshall, “A Formal Specification of Line Representations on Graphics Devices,” in Lecture Notes in Computer Science Volumne 186 ,Springer-Verlag (1985).

    Google Scholar 

  37. M. Martins and J. N. Oliveira, “Graphics Programming with Archetypes,” in Proceedings of Euro graphics 85 ,ed. C. V. Vandoni, North Holland (1985).

    Google Scholar 

  38. M. Martins and J. N. Oliveira, “On the Specification of Archetype Oriented Graphics Editors,” Universidade do Minho, Braga, Portugal (1986).

    Google Scholar 

  39. A. D. McGettrick, The Definition of Programming Languages ,Cambridge University Press (1980).

    MATH  Google Scholar 

  40. 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).

    Google Scholar 

  41. C. Morgan, The Schema Language ,Programming Research Group, Oxford (1984).

    Google Scholar 

  42. 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).

    Article  MATH  Google Scholar 

  43. F. G. Pagan, Formal Specification of Programming Languages ,Prentice-Hall (1981).

    MATH  Google Scholar 

  44. G. J. Reynolds, “A Token Based Graphics System,” Computer Graphics Forum 5(2), pp. 139–146

    Article  MathSciNet  Google Scholar 

  45. D. Richter, “Mappings between Product Data Definitions,” in Proceedings of the Eurographics ’86 Conference ,ed. A. A. G. Requicha, North-Holland Publishing Company (1986).

    Google Scholar 

  46. D. S. H. Rosenthal, “A Framework for Specifying GKS,” X3H3/80-63, ANSI Document (1980).

    Google Scholar 

  47. I. H. Sorensen, “A Design of a Display Interface,” Programming Research Group, University of Oxford (1981).

    Google Scholar 

  48. J. E. Stoy, Denotational Semantics ,The MTT Press (1977).

    Google Scholar 

  49. B. Sufrin, “Z Handbook,” FORSITE Project, Programming Research Group, Oxford (1986).

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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

Publish with us

Policies and ethics