On the theory of specification, implementation, and parametrization of abstract data types

ABSTRACT. In the framework of a category spec of equational speoficatlons of abstract data types, tmplementations are defined to be certain pairs of morphlsms with a common target Th~s concept covers, among others, arbitrary recurslon schemes for defining the derived operations It is shown that for given single steps of a multilevel tmplementatlon, there is always a multtlevel tmplementatlon composed of these steps, but there ts no effective construction of th~s overall implementauon Some suggestions are gtven for practtcal composition of tmplementat~ons Utdlzmg pushouts Parametric specifications and parameter assignments are defined to be spectal morphlsms in spec, and parameter substitution ~s made precise by means of pushouts Since actual parameters can agam be parametrtc, parameter subsututton can be tterated. Thts tterauon ts shown to be assoctatwe Whtle the subject is being treated on a syntactical level in terms of speclfieauons, the imtlal algebra approach ts adopted as providing an appropriate semantics for spec~ficauons, and the effects of the present concepts and results on the initial algebras are studie