Reporting on an extended project concerning modularized software development, the authors present a number of  theorems  related to the compatibility of specifications generated at various steps in the development and refinement of software systems. The work relates to a particular specification technique using a module concept based on initial algebra semantics. The report includes detailed reviews of the module concept; operations for module structuring, refinement, and realization; and the categorical framework employed. On this basis, a proof is given of a general theorem establishing the compatibility of the operations employed in the technique.

While the resulting theorem may be correct as it stands, the presentation and the overall argument are entirely unsatisfactory. The techniques are given in such a breezy style that the reader is left wondering who is supposed to do what.

The introduction starts by talking about the design and implementation of large software systems, and refers to a number of programming languages that provide facilities for handling modules. One page into the introduction, however, the aim shifts: “the main aim of this paper is to present a categorical framework for all kinds of compatibility problems….” This raises the question of what is gained by using a categorical framework in this context, as compared to what has been used by other authors. The authors neither ask nor answer this question. The whole work is thus reduced to an arid exercise in formal algebra. In this exercise, the word “correct” is used with a formally defined meaning; no attempt is made to relate it to such intuitive notions as are invoked.

To this exercise the authors then add a few remarks relating to informal issues, but these largely take the form of unsupported and misleading claims. For example, they suggest in Section 1.1 that proofs depend on the concepts being expressed within a formal syntax and semantics. This would invalidate many of the proofs given in the report, which depend on the reader’s insight into the figures shown.

The problems of modularized software development are undoubtedly in great need of systematic study. Unfortunately, the authors confine their attention to formality and superficial claims. They do not contribute to our insight.