Data Type Specification: Parameterization and the Power of Specification Techniques

Abstract

Our earlier work on abstract data types is extended by the answers to a number of questions on the power and limitations of algebraic specification techniques and by an algebraic treatment of parameterized data types like sets-of-( ) and stacks-of-(). The "hidden function" problem (the need to include operations in specifications which are wanted hidden from the user) is investigated; the relative power of conditional specifications and equational specifications is investigated; and it is shown that parameterized specifications must contain "side conditions" (e.g., that finite-sets-of-d requires an equality predicate on d).