Formal Specification of Interactive Graphics Programming Languages
William R. Mallgren · 1983
Formal specifications of practical software systems are increasingly common; yet computer graphics systems are invariably described by informal means. The difficulty is the variety of special constructs that are needed in graphics programming. This dissertation develops specification techniques for graphics programming languages. The contributions include a language design framework that facilitates specification and a new specification technique that encompasses interactive control constructs. Important concepts associated with graphics programming, such as picture, graphical transformation, and hierarchic picture structure, are defined in terms of sets and partial functions. Examples of these concepts are then expressed as graphical data types, allowing them to be specified using the algebraic specification technique. Language primitives for controlling user interaction, including user input and displayed output, cannot be fully expressed using ordinary data types. Event algebras, an extension of the algebraic specification technique suitable for describing shared resource modules, are introduced and used to specify interaction primitives. A prototype graphics language, made up of the language Pascal, a collection of graphical data types for producing hierarchically structured, two-dimensional pictures, and some convenient interaction primitives, is presented and formally specified in its entirety. Specifications are also given for portions of two existing systems: the language XPL/G and the Core Graphics standards proposal. Finally, some special problems associated with verification of graphics programs are addressed, and properties of several programs written in the prototype language are proven formally.