(Heterogeneous) Structured Specifications in Logics Without Interpolation

LOPEZ POMBO, CARLOS GUSTAVO; FRIAS, MARCELO F.

Ewa Orlowska on Relational Methods in Logic and Computer Science

Springer International Publishing

Año: 2018; p. 403 - 439

The world of software development has become intrinsically het- erogeneous. Many formal languages have been made available to help analysts and designers model di↵erent aspects of software. Some examples in the logic realm are equational logic and classical first-order logic, propositional tem- poral 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 struc- turing 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 San- nella and Tarlecki. Afterwards, Borzyszkowski presented sucient 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.