The Design of Data Type Specifications

This paper is about the design of data types in creating a software system. The major point is to explore a means for specifying a data type which is independent of its eventual implementation. The particular style of specification, called algebraic axioms, is exhibited by axiomatizing many commonly used data types. As such, these examples reveal a great deal about the intricacies of data type specification via algebraic axioms, and, in addition, provide a standard to which alternative forms may be compared. Further uses of this specification technique are in proving the correctness of implementations and in interpretively executing a large system design before actual implementation commences.