Formal specification of a small example based on GKS

ABSTRACT

Implicit regeneration is a fundamental concept of the Graphical Kernel System (GKS), an IS0 International Standard, but it is difficult to understand as presented in the English language specification of GKS. Consequently, it is a good example to use in determining whether formal specification techniques can be used effectively to describe and clarify graphics concepts of this kind. The problem is first motivated informally with a description of GKS concepts and terminology. A formal specification of implicit regeneration using a simplified model is then presented, and the notation that is used for its formalization (VDM) is described. Finally, properties of implicit regeneration are formulated and the specification is proved to conform to these properties. This demonstrates the applicability of formal specification to graphics software, because a sufficiently precise description of a complicated concept is provided that enables its consistency to be checked against an intuitive understanding of the concept as derived from the GKS document.

REFERENCES

• 1: BONO, P. R., ENCARNACAO, J., HOPGOOD, F. R. A., AND TEN HAGEN, P. J.W. GKS--The first graphics standard. IEEE Comput. Graph. Appl. (July 1982), 9-23.
• 2: CARSON, G.S. An approach to the formal specification of computer graphics systems. Comput. Graph. 8, 1 (1984), 51-58.
• 3: CARSON, G.S. The specification of computer graphics systems. {EEE Comput. Graph. Appl. (Sept. 1983), 27-41.
• 4: D A Duce , E V C Fielding, Better understanding through formal specification, Computer Graphics Forum, v.4 n.4, p.333-348, Dec. 1985 [doi>10.1111/j.1467-8659.1985.tb00238.x]
• 5: D. A. Duce , V. D. Fielding, Formal specification- a comparison of two techniques, The Computer Journal, v.30 n.4, p.316-327, Aug. 1987 [doi>10.1093/comjnl/30.4.316]
• 6: DUCE, D. A., AND FIELDING, E. V.C. Formal specificationmOn multiple workstations in GKS. Internal Working Paper, Rutherford Appleton Laboratory, Chilton, Didcot, England, 1985.
• 7: DUCE, D. A., AND FIELDING, E. V. C. Towards a formal specification of the GKS output primitives. In Proceedings of Eurographics 86. North-Holland, Amsterdam, 1986.
• 8: FIELDING, E. V.C. The specification of abstract mappings and their implementation as B+- trees. Tech. Monograph PRG-18, Programming Research Group, Oxford Univ. Computing Laboratory, Oxford, England, Sept. 1980.
• 9: GNATZ, R. An algebraic approach to the standardization and the certification of graphics software. Comput. Graph. Forum 2, 2/3 (1983).
• 10: GNATZ, R. Approaching a formal framework for graphics software standards. Comput. Graph. 8, 1 (1984), 39-50.
• 11: F. R.A. Hopgood , D. A. Duce , J. R. Gallop , D. C. Sutcliffe, Introduction to the Graphical Kernel System (GKS) (2nd ed. revised for international standard), Academic Press Ltd., London, UK, 1986
• 12: ISO. Information processing systems--Computer graphics--Graphical Kernel System (GKS) functional description. ISO 7942, ISO Central Secretariat, Geneva, 1985. Available from American National Standards Institute, New York.
• 13: Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 14: JONES, C.B. Systematic program development. Dept. of Computer Science, Univ. of Manchester, Manchester, England, 1984.
• 15: William R. Mallgren, Formal Specification of Graphic Data Types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.687-710, Oct. 1982 [doi>10.1145/69622.357191]
• 16: SUFRIN, B. Towards a formal specification of the ICL Data Dictionary. ICL Tech. J. (Nov. 1984), 195-217.
• 17: SUTCLIFFE, D.C. Attribute handling in GKS. In Proceedings o/Eurographics 82. North-Holland, Amsterdam, 1982.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.3 COMPUTER GRAPHICS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  I. Computing Methodologies
  I.3 COMPUTER GRAPHICS
      I.3.4 Graphics Utilities

          Nouns: GKS

General Terms:
Design, Standardization, Verification