(Heterogeneous) Structured Specifications in Logics Without Interpolation

Abstract

The world of software development has become intrinsically heterogeneous. Many formal languages have been made available to help analysts and designers model different aspects of software. Some examples in the logic realm are equational logic and classical first-order logic, propositional temporal logics such as LTL and CTL (and their first-order versions), multimodal logics such as the dynamic logic PDL and its first-order version, etc. One important feature of a specification language is the existence of structuring mechanisms enabling the modular construction of system descriptions. Structured specifications were introduced by Wirsing for first-order logic, and later presented in the language-independent setting of institutions by Sannella and Tarlecki. Afterwards, Borzyszkowski presented sufficient conditions for a calculus for (homogeneous) structured specifications to be complete. These conditions include some form of Craig’s interpolation, which results in a scenario that excludes many formalisms employed in the description of software. The contributions of this article are then summarised as follows: (a) We present a calculus for structured specifications whose completeness proof does not require any form of interpolation. (b) We extend this calculus to a complete calculus for heterogeneous structured specifications.