Toward Realistic Formal Specifications for Non-Trivial Graphical Objects

Abstract

Formal specification has long been advocated in programming methodology, and is becoming increasingly popular in computer graphics to characterise the semantics of components of graphics systems. Unfortunately, formal specifications tend to sacrifice realism for abstraction. The result is often a specification that is not as relevant to real graphics systems as it could be. This paper suggests that the use of sharper mathematical tools, together with the use of object orientation (i.e., data abstraction with inheritance) provides a way of resolving this problem. As an example, we attempt to specify formally classes of bitmaps and images. These are particularly interesting choices, for bitmaps and images are mutable, bitmaps can have a perceived effect on images, and their semantics depends on context.