A Formal Specification of a Boundary Representation

Abstract

Geometric modellers are used in a wide spectrum of applications in computer graphics. As many other applications use the generated internal representation of solids, semantic correctness is of special importance. On the other hand, the methodology of formal specification offers, in particular, the advantage of ensuring correctness by mathematical means. It is therefore a good idea to formally specify a geometric modeller. This paper describes an abstract data type defining a boundary representation. Special attention is paid to the operations for manipulating solids, i.e. the so-called Euler operations. The operation mfe (make face & edge) is used to show in detail how pre- and post-condition can be derived. Finally, mappings of this abstract data type onto implementations with different data models are discussed.