On Normal Forms for Structured Specifications with Generating Constraints

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


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.



Thanks to the anonymous referees for their constructive comments.


  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). 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). 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). 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). 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). 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). CrossRefGoogle Scholar
  16. [Mos04]
    Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004). 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). 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