We generalise and clarify connections between variants of modularity (preservation of faithfulness) and interpolation by localising them to a diagram in an entailment system. The variants of modularity arise naturally from the idea of building specifications in steps. We establish, by an algebraic approach, connections between these variants and (the existence of) versions of interpolating specifications. We also extend these correspondences to specification and interpolating families, and clarify the role of pushout diagrams in this context.
- Formal specifications
- Software engineering