Detecting equivalence of modular specifications with categorical diagrams

The composition of modular specifications can be modeled, in a category theoretic framework, by colimits of diagrams. Pushouts in particular describe the combination of two specifications sharing a common part. In this paper, we propose to represent the combination of modular specification as diagrams. First, we define a term language to represent modular specifications built with colimit constructions over a category of base specifications. Then, we propose to associate with each term a diagram. This interpretation provides us with a more abstract representation of modular specifications because irrelevant steps of the construction are eliminated. Finally, we propose an algorithm to normalize diagrams, in the case when the base category is skeletal, finite and cycle free. This allows us to detect "construction isomorphisms" between modular specifications, i.e. isomorphisms which do not depend on the semantics of the base specifications, but only on their combination. (C) 2000 Elsevier Science B.V. Ail rights reserved.