Formal Specification of Graphic Data Types

Abstract

Formal specification techniques and data abstractions have seen little application to computer graphics. Many of the objects and operations unique to graphics programs can be handled conveniently by def'ming special graphic data types. Not only do graphic data types provide an attractive way to work with pictures, but they also allow specification techniques for data abstractions to be employed. Algebraic axioms, because of their definitional nature, are especially well suited to specifying the diversity of types useful in graphics applications. In this paper, definitions are given for some important concepts that appear in graphics programs. Based on these definitions, some illustrative graphic data types, called point, region, geometric function, graphic transformation, and tree-structured picture, are defined and specified algebraically. A simple graphics language for line drawings is created by embedding these new data types in the language PASCAL. Using the specifications, an outline of a correctness proof for a small programming example is presented. © 1982, ACM. All rights reserved.