View article

Hierarchical abstract data types are algebraic specifications of computation structures where certain sorts, function symbols, and axioms are designated as being primitive. On hierarchical abstract data types additional structure is imposed. An algebraic specification is thus decomposed into several well-separated levels, such that both the understanding and the independent implementation of the levels is supported. This paper provides both model-theoretic and deduction-oriented conditions guaranteeing the soundness of a hierarchical specification. Furthermore necessary and sufficient conditions for the existence of initial and terminal models are investigated, and their close connection to the soundness of a hierarchy is demonstrated. In order to provide freedom and flexibility for specifications a wide class of axioms — namely universal-existential formulas — are admitted.