Skip to main content
SpringerLink
Log in

(Heterogeneous) Structured Specifications in Logics Without Interpolation

  • Chapter
  • First Online:
Ewa Orłowska on Relational Methods in Logic and Computer Science

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 17))

  • 217 Accesses

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.

Author’s research was supported by grants PICT 2013-2129 from ANPCyT – Agencia Nacional de Promoción Científica y Tecnológica, and PIP 11220130100148CO from CONICET – Concejo Nacional de Investigaciones Científicas y Técnicas.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Given \(\sigma : \varSigma \rightarrow \varSigma '\) a morphism in \(\mathsf {Sign}\), the corresponding morphism in the opposite category \(\mathsf {Sign^\mathsf{op}}\) will be denoted as \(\sigma ^\mathsf{op}\).

  2. 2.

    Once again, the reader should note the difference between \({\vdash ^\mathbb {I}}^\varSigma \), the entailment relation associated to \(\mathbb {I}\), and \({\vdash ^\mathbb {I}}_\varSigma \), the entailment relation for structured specifications over \(\mathbb {I}\).

References

  • Abadi, M. (1988). The Power of Temporal Proofs. Palo Alto, CA 94301, USA (Technical report No. 30).

    Google Scholar 

  • Abadi, M. & Manna, Z. (1990). Nonclausal deduction in first-order temporal logic. Journal of the ACM, 37(2), 279–317.

    Article  Google Scholar 

  • Astesiano, E. & Cerioli, M. (1991). Relationships between logical frameworks. In M. Bidoit & C. Choppy (Eds.), Recent Trends in Data Type Specification, 8th Workshop on Specification of Abstract Data Types Joint with the 3rd Compass Workshop, Selected Papers (Vol. 655, pp. 126–143). Lecture Notes in Computer Science. Dourdan: Springer.

    Chapter  Google Scholar 

  • Bergstra, J. A., Heering, J., & Klint, P. (1990). Module algebra. Journal of the ACM, 37(2), 335–372.

    Article  Google Scholar 

  • Booch, G., Rumbaugh, J., & Jacobson, I. (1998). The Unified Modeling Language User Guide. Boston: Addison-Wesley Longman Publishing Co., Inc.

    Google Scholar 

  • Borzyszkowski, T. (1997). In F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Selected Papers (Vol. 1376, pp. 107–121). Lecture Notes in Computer Science. Tarquinia: Springer.

    Google Scholar 

  • Borzyszkowski, T. (1998). Moving specification structures between logical systems. In J. L. Fiadeiro (Ed.), Recent Trends in Algebraic Development Techniques, 13th International Workshop, WADT’98, Selected Papers (Vol. 1589, pp. 16–30). Lecture Notes in Computer Science. Lisbon: Springer.

    Chapter  Google Scholar 

  • Borzyszkowski, T. (2002). Logical systems for structured specifications. Theoretical Computer Science, 286(2), 197–245.

    Article  Google Scholar 

  • Broy, M. & Cengarle, M. V. (2011). UML formal semantics: Lessons learned. Software and System Modeling, 10(4), 441–446.

    Article  Google Scholar 

  • Cengarle, M. V., Knapp, A., Tarlecki, A., & Wirsing, M. (2008). A heterogeneous approach to UML semantics. In P. Degano, R. D. Nicola, & J. Meseguer (Eds.), Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of his 65th Birthday (Vol. 5065, pp. 383–402). Lecture Notes in Computer Science. Berlin: Springer.

    Chapter  Google Scholar 

  • Cerioli, M. (1993). Relationships Between Logical Formalisms (Doctoral dissertation, Dipartamento di Informatica, Universitá degli studi di Pisa). Unpublished.

    Google Scholar 

  • Cerioli, M. & Meseguer, J. (1997). May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173(2), 311–347.

    Article  Google Scholar 

  • Clarke, E. M., Emerson, E. A., & Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 244–263.

    Article  Google Scholar 

  • Craig, W. (1957). Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22(3), 269–285.

    Article  Google Scholar 

  • de Lavalette, G. R. R., Kooi, B. P., & Verbrugge, R. (2008). Strong completeness and limited canonicity for PDL. Journal of Logic, Language and Information, 17(1), 69–87.

    Article  Google Scholar 

  • Diaconescu, R. (1998). Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. Applied Categorical Structures, 6(4), 427–453.

    Article  Google Scholar 

  • Diaconescu, R. (2002). Grothendieck institutions. Applied Categorical Structures, 10(4), 383–402.

    Article  Google Scholar 

  • Diaconescu, R. (Ed.). (2008). Institution-independent Model Theory. Basel: Birkhäuser.

    Google Scholar 

  • Diaconescu, R. & Futatsugi, K. (2002). Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2), 289–318.

    Article  Google Scholar 

  • Diaconescu, R., Goguen, J. A., & Stefaneas, P. (1993). Logical support for modularisation. In Papers Presented at the 2nd Annual Workshop on Logical Environments (pp. 83–130). Edinburgh: Cambridge University Press.

    Google Scholar 

  • Dimitrakos, T. & Maibaum, T. S. E. (2000). On a generalized modularization theorem. Information Processing Letters, 74(1–2), 65–71.

    Article  Google Scholar 

  • Emerson, E. A. & Halpern, J. Y. (1985). Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1), 1–24.

    Article  Google Scholar 

  • Emerson, E. A. & Halpern, J. Y. (1986). “sometimes” and “not never” revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1), 151–178.

    Article  Google Scholar 

  • Fine, K. (1979). Failures of the interpolation lemma in quantified modal logic. Journal of Symbolic Logic, 44(2), 201–206.

    Article  Google Scholar 

  • Frias, M. F. (2002). Fork Algebras in Algebra, Logic and Computer Science. Advances in Logic. Singapore: World Scientific.

    Google Scholar 

  • Frias, M. F., Baum, G., & Haeberer, A. M. (1997). Fork algebras in algebra, logic and computer science. Fundamenta Informaticae, 32(1), 1–25.

    Article  Google Scholar 

  • Frias, M. F., Baum, G., & Haeberer, A. M. (1998). Representability and program construction within fork algebras. Logic Journal of the IGPL, 6(2), 227–257.

    Article  Google Scholar 

  • Frias, M. F., Baum, G., & Maibaum, T. S. E. (2002) In H. C. M. de Swart (Ed.), Relational Methods in Computer Science. RelMiCS 2001 (Vol. 2561, pp. 66–80). Lecture Notes in Computer Science. Berlin: Springer.

    Google Scholar 

  • Frias, M. F., Haeberer, A. M., & Veloso, P. A. S. (1997). A finite axiomatization for fork algebras. Logic Journal of the IGPL, 5(3), 1–10.

    Article  Google Scholar 

  • Frias, M. F. & López Pombo, C. (2006). Interpretability of first-order linear temporal logics in fork algebras. Journal of Logic and Algebraic Programming, 66(2), 161–184.

    Article  Google Scholar 

  • Frias, M. F. & López Pombo, C. G. (2003). Time is on my side. Proceedings of the 7th International Workshop on Relational Methods in Computer Science RelMiCS 2003. Malente, Germany (pp. 105–111).

    Google Scholar 

  • Frias, M. F. & Orłowska, E. (1995). A proof system for fork algebras and its applications to reasoning in logics based on intuitionism. Logique et Analyse, 38(150–152), 239–284.

    Google Scholar 

  • Frias, M. F. & Orłowska, E. (1998). Equational reasoning in nonclassical logics. Journal of Applied Non-classical Logics, 8(1–2), 27–66.

    Article  Google Scholar 

  • Goguen, J. A. & Burstall, R. M. (1983). Introducing institutions. In E. M. Clarke & D. Kozen (Eds.), Proceedings of Logics of Programs, Workshop 1983 (Vol. 164, pp. 221–256). Lecture Notes in Computer Science. Pittsburgh: Springer.

    Chapter  Google Scholar 

  • Goguen, J. A. & Burstall, R. M. (1992). Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1), 95–146.

    Article  Google Scholar 

  • Goguen, J. A. & Rou, G. (2002). Institution morphisms. Formal Aspects of Computing, 13(3–5), 274–307.

    Article  Google Scholar 

  • Gyuris, V. (1997). A short proof of representability of fork algebras. Theoretical Computer Science, 188(1–2), 211–220.

    Article  Google Scholar 

  • Haeberer, A. M. & Veloso, P. A. (1991). Partial relations for program derivation: Adequacy, inevitability and expressiveness. In B. Möller (Ed.), Proceedings of IFIP TC2 Working Conference on Constructing Programs from Specifications 1991 (pp. 310–352). Pacific Grove: North Holland.

    Google Scholar 

  • Harel, D. (2001). Dynamic logic. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. 2, pp. 135–165). Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  • Harel, D., Kozen, D., & Tiuryn, J. (2000). Dynamic Logic. Cambridge: MIT Press.

    Google Scholar 

  • Kowalski, T. (2002). PDL has interpolation. Journal of Symbolic Logic, 67(3), 933–946.

    Article  Google Scholar 

  • Kowalski, T. (2004). Retraction note for “PDL has interpolation”. Journal of Symbolic Logic, 69(3), 935.

    Article  Google Scholar 

  • López Pombo, C. G. (2007). Fork Algebras as a Tool for Reasoning Across Heterogeneous Specifications (Doctoral dissertation, Departamento de Computación. Facultad de Ciencias Exactas y Naturales: Universidad de Buenos Aires). Unpublished.

    Google Scholar 

  • López Pombo, C. G. & Frias, M. F. (2006). Fork algebras as a sufficiently rich universal institution. In M. Johnson & V. Vene (Eds.), Proceedings of Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006 (Vol. 4019, pp. 235–247). Lecture Notes in Computer Science. Kuressaare: Springer.

    Chapter  Google Scholar 

  • Maksimova, L. (1990). Temporal logics with “the next” operator do not have interpolation. Ibirskii Matematicheskii Zhurnal, 32(6), 989–993.

    Google Scholar 

  • Manna, Z. & Pnueli, A. (1995). Temporal Verification of Reactive Systems–Safety. Berlin: Springer.

    Chapter  Google Scholar 

  • Martini, A. & Wolter, U. (1997). A systematic study of mappings between institutions. In F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Selected Papers (Vol. 1376, pp. 300–315). Lecture Notes in Computer Science. Tarquinia: Springer.

    Chapter  Google Scholar 

  • Martini, A. & Wolter, U. (1998). A single perspective on arrows between institutions. In A. M. Haeberer (Ed.), Proceedings of Algebraic Methodology and Software Technology, 7th International Conference, AMAST ’98 (Vol. 1548, pp. 486–501). Lecture Notes in Computer Science. Amazonia: Springer.

    Chapter  Google Scholar 

  • McLane, S. (1971). Categories for Working Mathematician. New York: Springer.

    Google Scholar 

  • Meseguer, J. (1987). General logics. In H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, D. Lascar, & M. Rodríguez-Artajelo (Eds.), Proceedings of the Logic Colloquium’87 (Vol. 129, pp. 275–329). Studies in Logic and the Foundations of Mathematics. Granada: North Holland.

    Google Scholar 

  • Mossakowski, T., Maeder, C., & Lüttich, K. (2007). The heterogeneous tool sets, hets. In O. Grumberg & M. Huth (Eds.), Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 (Vol. 4424, pp. 519–522). Lecture Notes in Computer Science. Braga: Springer.

    Google Scholar 

  • Mossakowski, T. & Tarlecki, A. (2009). Heterogeneous logical environments for distributed specifications. In A. Corradini & U. Montanari (Eds.), Recent Trends in Algebraic Development Techniques, Proceedings of the 19th International Workshop in Algebraic Development Techniques, WADT 2008 (Vol. 5486, pp. 266–289). Lecture Notes in Computer Science. Berlin: Springer.

    Chapter  Google Scholar 

  • Mossakowski, T. & Tarlecki, A. (2014). A relatively complete calculus for structured heterogeneous specifications. In A. Muscholl (Ed.), Proceedings of Foundations of Software Science and Computation Structures–17th International Conference, FOSSACS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 (Vol. 8412, pp. 441–456). Lecture Notes in Computer Science. Grenoble: Springer.

    Google Scholar 

  • Orłowska, E. & Golińska-Pilarek, J. (2011). Dual tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.

    Book  Google Scholar 

  • Parnas, D. L. (1972). On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12), 1053–1058.

    Article  Google Scholar 

  • Parnas, D. L. (1978). Designing software for ease of extension and contraction. In M. V. Wilkes, L. A. Belady, Y. H. Su, H. Hayman, & P. H. E. Jr. (Eds.), Proceedings of the 3rd International Conference on Software Engineering 1978 (pp. 264–277). Atlanta: IEEE Computer Society.

    Google Scholar 

  • Parnas, D. L. (1979). Designing software for ease of extension and contraction. IEEE Transactions on Software Engineering, 5(2), 128–138. See also (Parnas, 1978).

    Article  Google Scholar 

  • Pnueli, A. (1977). The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science 1977 (pp. 46–57). Providence: IEEE Computer Society.

    Google Scholar 

  • Pnueli, A. (1981). The temporal semantics of concurrent programs. Theoretical Computer Science, 13, 45–60.

    Article  Google Scholar 

  • Reynolds, M. (2001). An axiomatization of full computation tree logic. Journal of Symbolic Logic, 66(3), 1011–1057.

    Article  Google Scholar 

  • Rou, G. & Goguen, J. A. (2000). On equational craig interpolation. Journal of Universal Computer Science, 6(1), 194–200.

    Google Scholar 

  • Sannella, D. & Tarlecki, A. (1988). Specifications in an arbitrary institution. Information and Computation, 76(2/3), 165–210.

    Article  Google Scholar 

  • Sannella, D. & Tarlecki, A. (2012). Foundations of Algebraic Specification and Formal Software Development., Monographs in Theoretical Computer Science. An EATCS Series Berlin: Springer.

    Book  Google Scholar 

  • Sannella, D. & Tarlecki, A. (2014). Property-oriented semantics of structured specifications. Mathematical Structures in Computer Science, 24(2), e240205.

    Google Scholar 

  • Tarlecki, A. (1986). Bits and pieces of the theory of institutions. In D. H. Pitt, S. Abramsky, A. Poigné, & D. E. Rydeheard (Eds.), Category Theory and Computer Programming, Tutorial and Workshop, Guildford, UK, September 16–20, 1985 Proceedings (Vol. 240, pp. 334–363). Lecture Notes in Computer Science. Guildford: Springer.

    Google Scholar 

  • Tarlecki, A. (1995). Moving between logical systems. In M. Haveraaen, O. Owe, & O.-J. Dahl (Eds.), Recent Trends in Data Type Specification, 11th Workshop on Specification of Abstract Data Types Joint with the 8th Compass Workshop 1995, Selected Papers (Vol. 1130, pp. 478-502). Lecture Notes in Computer Science. Oslo: Springer.

    Chapter  Google Scholar 

  • Tarlecki, A. (2000). Towards heterogeneous specifications. In D. Gabbay & M. de Rijke (Eds.), Frontiers of Combining Systems (Vol. 2, pp. 337–360). Hertfordshire: Research Studies Press.

    Google Scholar 

  • Tarlecki, A. (2003). Abstract specification theory: An overview. In M. Broy & M. Pizka (Eds.), Proceedings of the NATO Advanced Study Institute on Models, Algebras and Logic of Engineering Software (pp. 43–79). Amsterdam: IOS Press.

    Google Scholar 

  • Wirsing, M. (1991). Structured specifications: Syntax, semantics, and proof calculus. In F. L. Bauer, W. Brauer, & H. Schwichtenberg (Eds.), Proceedings of the NATO Advanced Study Institute on Models, Algebras and Logic of Engineering Software (pp. 411–442). Amsterdam: IOS Press.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad de Buenos Aires, Facultad de Ciencias Exactas y Naturales, Departamento de Computación and CONICET–Universidad de Buenos Aires, Instituto de Investigación en Ciencias de la Computación (ICC), Pabellón I, Ciudad Universitaria, C1428EGA, Ciudad Autónoma de Buenos Aires, Buenos Aires, Argentina

    Carlos Gustavo Lopez Pombo

  2. Department of Software Engineering, Buenos Aires Institute of Technology (ITBA) and Consejo Nacional de Investigaciones Científicas y Tecnológicas (CONICET), Av. Eduardo Madero 399, C1106ACD, Ciudad Autónoma de Buenos Aires, Buenos Aires, Argentina

    Marcelo Frias

Authors
  1. Carlos Gustavo Lopez Pombo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marcelo Frias
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carlos Gustavo Lopez Pombo .

Editor information

Editors and Affiliations

  1. Institute of Philosophy, University of Warsaw, Warsaw, Poland

    Joanna Golińska-Pilarek

  2. Department of Logic and Methodology of Science, University of Lodz, Łódź, Poland

    Michał Zawidzki

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Lopez Pombo, C.G., Frias, M. (2018). (Heterogeneous) Structured Specifications in Logics Without Interpolation. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_16

Download citation

Publish with us

Policies and ethics

Search

Navigation