Advertisement

Parchments for CafeOBJ Logics

  • Till Mossakowski
  • Wiesław Pawłowski
  • Donald Sannella
  • Andrzej Tarlecki
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)

Abstract

This paper addresses issues arising in the systematic construction of large logical systems. We rely on a model-theoretic view of logical systems, captured by institutions that are in turn presented by parchments. We define their categories, and study constructions that may be carried out in these categories. In particular we show how limits of parchments may be used to combine features involved in various logical systems, sometimes necessarily augmenting the universal construction by additional systematic adjustments. We illustrate these developments by sketching how the logical systems that form the logical foundations of CafeOBJ may be built in this manner.

Keywords

Natural Transformation Logical System Evaluation Structure Satisfaction Condition Behavioural Signature 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BD94]
    Burstall, R., Diaconescu, R.: Hiding and behaviour: An institutional approach. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 75–92. Prentice-Hall (1994)Google Scholar
  2. [BG80]
    Burstall, R.M., Goguen, J.A.: The semantics of Clear, a specification language. In: Bjørner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  3. [BH06]
    Bidoit, M., Hennicker, R.: Constructor-based observational logic. Journal of Logic and Algebraic Programming 67(1-2), 3–51 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  4. [CGR03]
    Caleiro, C., Gouveia, P., Ramos, J.: Completeness results for fibred parchments: Beyond the propositional base. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 185–200. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. [CHK+11]
    Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project abstract: Logic atlas and integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 289–291. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. [CHK+12]
    Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F., Sojakova, K.: Towards logical frameworks in the heterogeneous tool set Hets. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 139–159. Springer, Heidelberg (2012)Google Scholar
  7. [CMRS01]
    Caleiro, C., Mateus, P., Ramos, J., Sernadas, A.: Combining logics: Parchments revisited. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 48–70. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. [DF98]
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific (1998), See also http://www.ldl.jaist.ac.jp/cafeobj/
  9. [DF02]
    Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  10. [Dia02]
    Diaconescu, R.: Grothendieck institutions. Applied Categorical Structures 10(4), 383–402 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  11. [Dia07]
    Diaconescu, R.: A methodological guide to the CafeOBJ logic. In: Bjørner, D., Henson, M.C. (eds.) Logics of Specification Languages, Monographs in Theoretical Computer Science, pp. 153–240. Springer, Heidelberg (2007)Google Scholar
  12. [Dia08]
    Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)Google Scholar
  13. [Dia11]
    Diaconescu, R.: Grothendieck inclusion systems. Applied Categorical Structures 19(5), 783–802 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  14. [FC96]
    Fiadeiro, J.L., Costa, J.F.: Mirror, mirror in my hand: A duality between specifications and models of process behaviour. Mathematical Structures in Computer Science 6(4), 353–373 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  15. [GB86]
    Goguen, J.A., Burstall, R.M.: A study in the functions of programming methodology: Specifications, institutions, charters and parchments. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 313–333. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  16. [GB92]
    Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  17. [GM92]
    Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105(2), 217–273 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  18. [GR02]
    Goguen, J.A., Roşu, G.: Institution morphisms. Formal Aspects of Computing 13(3-5), 274–307 (2002)CrossRefzbMATHGoogle Scholar
  19. [GWM+00]
    Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ3. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action. Kluwer (2000)Google Scholar
  20. [Mac71]
    Mac Lane, S.: Categories for the Working Mathematician. Springer (1971)Google Scholar
  21. [Mes98]
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  22. [MML07]
    Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007), See also http://www.informatik.uni-bremen.de/cofi/hets/
  23. [Mos96]
    Mossakowski, T.: Using limits of parchments to systematically construct institutions of partial algebras. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.) WADT 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 379–393. Springer, Heidelberg (1996)Google Scholar
  24. [Mos03]
    Mossakowski, T.: Foundations of heterogeneous specification. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 359–375. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  25. [Mos05]
    Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis, Universität Bremen (2005)Google Scholar
  26. [MT09]
    Mossakowski, T., Tarlecki, A.: Heterogeneous logical environments for distributed specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 266–289. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  27. [MTP97]
    Mossakowski, T., Tarlecki, A., Pawłowski, W.: Combining and representing logical systems. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 177–196. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  28. [MTP98]
    Mossakowski, T., Tarlecki, A., Pawłowski, W.: Combining and representing logical systems using model-theoretic parchments. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 349–364. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  29. [ST87]
    Sannella, D., Tarlecki, A.: On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34, 150–178 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  30. [ST88]
    Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76(2-3), 165–210 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  31. [ST12]
    Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer (2012)Google Scholar
  32. [SW83]
    Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413–427. Springer, Heidelberg (1983)Google Scholar
  33. [Tar86]
    Tarlecki, A.: Bits and pieces of the theory of institutions. In: Pitt, D.H., Abramsky, S., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 334–360. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  34. [Tar96]
    Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.) WADT 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)Google Scholar
  35. [Tar00]
    Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems 2. Studies in Logic and Computation, pp. 337–360. Research Studies Press (2000)Google Scholar
  36. [TBG91]
    Tarlecki, A., Burstall, R.M., Goguen, J.A.: Some fundamental algebraic tools for the semantics of computation. Part 3: Indexed categories. Theoretical Computer Science 91(2), 239–264 (1991)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Till Mossakowski
    • 1
  • Wiesław Pawłowski
    • 2
  • Donald Sannella
    • 3
  • Andrzej Tarlecki
    • 4
  1. 1.Faculty of Computer ScienceUniversity of MagdeburgGermany
  2. 2.Institute of InformaticsUniversity of GdańskPoland
  3. 3.Laboratory for Foundations of Computer ScienceUniversity of EdinburghUK
  4. 4.Institute of InformaticsUniversity of WarsawPoland

Personalised recommendations