Advertisement

On Normal Forms for Structured Specifications with Generating Constraints

  • Donald SannellaEmail author
  • Andrzej Tarlecki
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10800)

Abstract

Hartmut Ehrig and others in [EWT83] studied normal form results for complex generating constraints imposed on basic specifications. Since then this work has been followed by subsequent results concerning normal forms for structured specifications, typically built from basic specifications using union, translation and hiding. We consider generating constraints as additional specification-building operations and follow and extend the results concerning normal forms for the resulting specifications with various forms of generating constraints.

Notes

Acknowledgements

Thanks to the anonymous referees for their constructive comments.

References

  1. [Awo06]
    Awodey, S.: Category Theory. Oxford University Press, New York (2006)CrossRefzbMATHGoogle Scholar
  2. [BCH+04]
    Baumeister, H., Cerioli, M., Haxthausen, A., Mossakowski, T., Mosses, P.D., Sannella, D., Tarlecki, A.: Casl semantics. In: [Mos04] (2004)Google Scholar
  3. [BHK90]
    Bergstra, J.A., Heering, J., Klint, P.: Module algebra. J. Assoc. Comput. Mach. 37(2), 335–372 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  4. [BM04]
    Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004).  https://doi.org/10.1007/b11968. http://www.informatik.uni-bremen.de/cofi/index.php/CASL zbMATHGoogle Scholar
  5. [Bor02]
    Borzyszkowski, T.: Logical systems for structured specifications. Theor. Comput. Sci. 286(2), 197–245 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  6. [CMST17]
    Codescu, M., Mossakowski, T., Sannella, D., Tarlecki, A.: Specification refinements: calculi, tools, and applications. Sci. Comput. Program. 144, 1–49 (2017)CrossRefGoogle Scholar
  7. [CR97]
    Căzănescu, V.E., Roşu, G.: Weak inclusion systems. Math. Struct. Comput. Sci. 7(2), 195–206 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  8. [DGS93]
    Diaconescu, R., Goguen, J.A., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Cambridge University Press, Cambridge (1993)Google Scholar
  9. [EM85]
    Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1. EATCS Monographs on Theoretical Computer Science, vol. 6. Springer, Heidelberg (1985).  https://doi.org/10.1007/978-3-642-69962-7 CrossRefzbMATHGoogle Scholar
  10. [EWT83]
    Ehrig, H., Wagner, E.G., Thatcher, J.W.: Algebraic specifications with generating constraints. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 188–202. Springer, Heidelberg (1983).  https://doi.org/10.1007/BFb0036909 CrossRefGoogle Scholar
  11. [GB84]
    Goguen, J.A., Burstall, R.M.: Introducing institutions. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 221–256. Springer, Heidelberg (1984).  https://doi.org/10.1007/3-540-12896-4_366. Many revised versions were widely circulated, with [GB92] as the endpointCrossRefGoogle Scholar
  12. [GB92]
    Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  13. [GR04]
    Goguen, J.A., Roşu, G.: Composing hidden information modules over inclusive institutions. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 96–123. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-39993-3_7 CrossRefGoogle Scholar
  14. [McC80]
    McCarthy, J.: Circumscription – a form of non-monotonic reasoning. Artif. Intell. 13(1–2), 27–39 (1980)CrossRefzbMATHGoogle Scholar
  15. [MCNK15]
    Mossakowski, T., Codescu, M., Neuhaus, F., Kutz, O.: The distributed ontology, modeling and specification language – DOL. In: Koslow, A., Buchsbaum, A. (eds.) The Road to Universal Logic. SUL, pp. 489–520. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-15368-1_21 CrossRefGoogle Scholar
  16. [Mos04]
    Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004).  https://doi.org/10.1007/b96103 zbMATHGoogle Scholar
  17. [MS85]
    MacQueen, D., Sannella, D.: Completeness of proof systems for equational specifications. IEEE Trans. Softw. Eng. SE–11(5), 454–461 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  18. [ST88]
    Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Inf. Comput. 76(2–3), 165–210 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  19. [ST12]
    Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012)CrossRefzbMATHGoogle Scholar
  20. [ST14]
    Sannella, D., Tarlecki, A.: Property-oriented semantics of structured specifications. Math. Struct. Comput. Sci. 24(2), e240205 (2014)MathSciNetzbMATHGoogle Scholar
  21. [SW83]
    Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation: extended abstract. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413–427. Springer, Heidelberg (1983).  https://doi.org/10.1007/3-540-12689-9_122 CrossRefGoogle Scholar
  22. [Tar83]
    Tarlecki, A.: Remarks on [EWT83]. Unpublished note, Department of Computer Science, University of Edinburgh (1983)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Laboratory for Foundations of Computer ScienceUniversity of EdinburghEdinburghUK
  2. 2.Institute of InformaticsUniversity of WarsawWarsawPoland

Personalised recommendations