Data type specification: Parameterization and the power of specification techniques

Abstract

This paper extends our earlier work on abstract data types by providing an algebraic treatment of parametrized data types (e.g., sets-of-( ), stacks-of-( ), etc.), as well as answering a number of questions on the power and limitations of algebraic specification techniques. In brief: we investigate the "hidden function" problem (the need to include operations in specifications which we want to be hidden from the user); we prove that conditional specifications are inherently more powerful than equational specifications; we show that parameterized specifications must contain "side conditions" (e.g., that finite-sets-of-d requires an equality predicate on d), and we compare the power of the algebraic approach taken here with the more categorical approach of Lehman and Smyth.