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.

There are two approaches to formal specification, algebraic techniques and constructive techniques. This paper compares representatives of these two approaches, OBJ, which is an algebraic technique, and VDM, which is a constructive technique. These approaches are compared in the context of an example taken from the ISO computer graphics standard, the Graphical Kernel System (GKS). The paper contains tutorial introductions to OBJ and VDM as well as a concise description of the GKS concepts contained in the example.

The literature contains a number of papers which look at the application of formal specification techniques to the specification of computer graphics systems [3,5,6,7,8,10,14]. A landmark in computer graphics was reached on 15 August 1985, with the publication of the Graphical Kernel System (GKS) as the first ISO standard for computer graphics programming [13]. This paper extends some of the ideas for defining graphics data types contained in [3] and [14] and applies them to GKS. Of particular interest, is a more formal definition of the geometry of the GKS output primitives than that given in the GKS document.

Abstract The Graphical Kernel System (GKS) is now registered as an ISO International Standard for computer graphics programming. One of the major innovations of the Standard is the bundled specification of aspects, a mechanism which gives the applications programmer the ability to tailor the appearance of a picture independently on each of the workstations on which it is displayed, using the capabilities of the workstations. GKS also incorporates the traditional method of individual specification of aspects in which each workstation does the best it can to represent global aspect values. In this paper a formal specification technique, the Vienna Development Method (VDM), is used to describe aspect specification. The GKS model of aspect specification is progressively constructed from simpler models. Properties of these simpler models are formulated and the specifications are proved to conform to these. The properties are then traced through the more complex models. The paper demonstrates the applicability of formal specification to the design of graphics software and the ability of formal techniques to catalyse the deeper understanding of designs.

A system for automatically generating programs for a particular class of problem – in this case the class of payroll problems – is discussed. The technique used in the generation process is based on the stepwise refinement approach to problem solving. The method described is applicable to other similar problems and ultimately could be used in a general automatic programming system.