Advertisement

(Heterogeneous) Structured Specifications in Logics Without Interpolation

  • Carlos Gustavo Lopez Pombo
  • Marcelo Frias
Chapter
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)

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.

Keywords

Structured specifications Heterogeneous specifications Institutions 

References

  1. Abadi, M. (1988). The Power of Temporal Proofs. Palo Alto, CA 94301, USA (Technical report No. 30).Google Scholar
  2. Abadi, M. & Manna, Z. (1990). Nonclausal deduction in first-order temporal logic. Journal of the ACM, 37(2), 279–317.Google Scholar
  3. 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.Google Scholar
  4. Bergstra, J. A., Heering, J., & Klint, P. (1990). Module algebra. Journal of the ACM, 37(2), 335–372.Google Scholar
  5. Booch, G., Rumbaugh, J., & Jacobson, I. (1998). The Unified Modeling Language User Guide. Boston: Addison-Wesley Longman Publishing Co., Inc.Google Scholar
  6. 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
  7. 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.Google Scholar
  8. Borzyszkowski, T. (2002). Logical systems for structured specifications. Theoretical Computer Science, 286(2), 197–245.Google Scholar
  9. Broy, M. & Cengarle, M. V. (2011). UML formal semantics: Lessons learned. Software and System Modeling, 10(4), 441–446.Google Scholar
  10. 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.Google Scholar
  11. Cerioli, M. (1993). Relationships Between Logical Formalisms (Doctoral dissertation, Dipartamento di Informatica, Universitá degli studi di Pisa). Unpublished.Google Scholar
  12. Cerioli, M. & Meseguer, J. (1997). May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173(2), 311–347.Google Scholar
  13. 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.Google Scholar
  14. 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.Google Scholar
  15. 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.Google Scholar
  16. Diaconescu, R. (1998). Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. Applied Categorical Structures, 6(4), 427–453.Google Scholar
  17. Diaconescu, R. (2002). Grothendieck institutions. Applied Categorical Structures, 10(4), 383–402.Google Scholar
  18. Diaconescu, R. (Ed.). (2008). Institution-independent Model Theory. Basel: Birkhäuser.Google Scholar
  19. Diaconescu, R. & Futatsugi, K. (2002). Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2), 289–318.Google Scholar
  20. 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
  21. Dimitrakos, T. & Maibaum, T. S. E. (2000). On a generalized modularization theorem. Information Processing Letters, 74(1–2), 65–71.Google Scholar
  22. 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.Google Scholar
  23. 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.Google Scholar
  24. Fine, K. (1979). Failures of the interpolation lemma in quantified modal logic. Journal of Symbolic Logic, 44(2), 201–206.Google Scholar
  25. Frias, M. F. (2002). Fork Algebras in Algebra, Logic and Computer Science. Advances in Logic. Singapore: World Scientific.Google Scholar
  26. Frias, M. F., Baum, G., & Haeberer, A. M. (1997). Fork algebras in algebra, logic and computer science. Fundamenta Informaticae, 32(1), 1–25.Google Scholar
  27. 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.Google Scholar
  28. 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
  29. 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.Google Scholar
  30. 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.Google Scholar
  31. 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
  32. 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
  33. Frias, M. F. & Orłowska, E. (1998). Equational reasoning in nonclassical logics. Journal of Applied Non-classical Logics, 8(1–2), 27–66.Google Scholar
  34. 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.Google Scholar
  35. Goguen, J. A. & Burstall, R. M. (1992). Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1), 95–146.Google Scholar
  36. Goguen, J. A. & Rou, G. (2002). Institution morphisms. Formal Aspects of Computing, 13(3–5), 274–307.Google Scholar
  37. Gyuris, V. (1997). A short proof of representability of fork algebras. Theoretical Computer Science, 188(1–2), 211–220.Google Scholar
  38. 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
  39. 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
  40. Harel, D., Kozen, D., & Tiuryn, J. (2000). Dynamic Logic. Cambridge: MIT Press.Google Scholar
  41. Kowalski, T. (2002). PDL has interpolation. Journal of Symbolic Logic, 67(3), 933–946.Google Scholar
  42. Kowalski, T. (2004). Retraction note for “PDL has interpolation”. Journal of Symbolic Logic, 69(3), 935.Google Scholar
  43. 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
  44. 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.Google Scholar
  45. Maksimova, L. (1990). Temporal logics with “the next” operator do not have interpolation. Ibirskii Matematicheskii Zhurnal, 32(6), 989–993.Google Scholar
  46. Manna, Z. & Pnueli, A. (1995). Temporal Verification of Reactive Systems–Safety. Berlin: Springer.Google Scholar
  47. 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.Google Scholar
  48. 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.Google Scholar
  49. McLane, S. (1971). Categories for Working Mathematician. New York: Springer.Google Scholar
  50. 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
  51. 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
  52. 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.Google Scholar
  53. 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
  54. Orłowska, E. & Golińska-Pilarek, J. (2011). Dual tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.Google Scholar
  55. Parnas, D. L. (1972). On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12), 1053–1058.Google Scholar
  56. 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
  57. 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).Google Scholar
  58. 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
  59. Pnueli, A. (1981). The temporal semantics of concurrent programs. Theoretical Computer Science, 13, 45–60.Google Scholar
  60. Reynolds, M. (2001). An axiomatization of full computation tree logic. Journal of Symbolic Logic, 66(3), 1011–1057.Google Scholar
  61. Rou, G. & Goguen, J. A. (2000). On equational craig interpolation. Journal of Universal Computer Science, 6(1), 194–200.Google Scholar
  62. Sannella, D. & Tarlecki, A. (1988). Specifications in an arbitrary institution. Information and Computation, 76(2/3), 165–210.Google Scholar
  63. Sannella, D. & Tarlecki, A. (2012). Foundations of Algebraic Specification and Formal Software Development., Monographs in Theoretical Computer Science. An EATCS Series Berlin: Springer.Google Scholar
  64. Sannella, D. & Tarlecki, A. (2014). Property-oriented semantics of structured specifications. Mathematical Structures in Computer Science, 24(2), e240205.Google Scholar
  65. 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
  66. 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.Google Scholar
  67. 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
  68. 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
  69. 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.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 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)Ciudad Autónoma de Buenos Aires, Buenos AiresArgentina
  2. 2.Department of Software EngineeringBuenos Aires Institute of Technology (ITBA) and Consejo Nacional de Investigaciones Científicas y Tecnológicas (CONICET)Ciudad Autónoma de Buenos Aires, Buenos AiresArgentina

Personalised recommendations