Design Strategies for Algebraic Specifications

Abstract

The algebraic specification of abstract data types can be affected by serious flaws. Rather than attempting, as it is usually done, to detect defects in a specification a posteriori, i.e., after the specification has been designed, we propose two strategies for addressing this problem a priori, i.e., during design phase of a specification. We investigate two common flaws of algebraic operations, under- and over-specification, determine sufficient and/or necessary conditions to avoid them, and show how to obtain these conditions in a constructive way. Our approach is based on the completeness and parsimony properties of sets of tuples and on a recursive mechanism which extends primitive recursion from natural numbers to abstract data types. Finally, we attempt to assess the power and the limitations of our approach and relate the properties on which it is based to other similar properties which have appeared in the literature. We formally prove a number of results and illustrate their application to the design of specifications by means of examples.