Small specifications for large finite data structures

Abstract

Having concerned ourselves with boundedness properties of algebraic data structure specifications in the sense of the ADJ Group (see [4, 6, 7]) before now—see [1], which is in a sense a follow-up of [3] of Bergstra and Tucker—we show in this paper that data structures of cardinality > n can be specified by means of a bounded number of equations, not depending on n, which are each of length O(n) only

Keywords:

• algebraic data structures
• equational and conditional specifications
• boundedness properties