Canonical Term Functors and Parameterization-by-use for the Specification of Abstract Data Types

Abstract

Algebraic and algorithmic specification methods for abstract data types are combined in the specification language ASPIK covering the whole scope from high level requirements and formal specifications to functional programs. The link between axiomatic and algorithmic specifications is provided by the notion of canonical term functor, a generalization of canonical term algebra. Specifications are structured hierarchically and the new concept of parameterization-by-use offers a flexible means to refine such hierarchies. These features are illustrated by several examples of ASPIK specifications.