Hennicker takes an observational approach to the construction of implementations of algebraic specifications. An implementation is correct if it satisfies the input/output behavior required by the specification, irrespective of its internal functions. The author presents a proof technique, called context induction, for the verification of implementations. He extends the approach to parameterized observational specifications to support modular construction of implementations.

It has been found that two observational implementations compose vertically (or stepwise). If at least one of the parameterized specifications P₁ or P₂ is monotonic, then they also compose horizontally (or modularly). For P_i to be monotonic, it must be parameter complete and parameter tolerant, and all observational non-parameter sorts of P_i must be observably monomorphic. Furthermore, for P_i to be parameter complete and parameter tolerant, a necessary and sufficient condition is that it must be parameter protecting (contain no junk and no confusion).

The paper contains useful comparisons with other approaches; excellent, clear examples illustrate the features covered. The paper is fairly long, but the proofs of  theorems  have been placed in the appendix. It would make more sense to the reader if the graphical illustrations for “vertical” and “horizontal” implementations were consistent with the literal meanings of the two words, as in the figures originally proposed by Burstall and Goguen.