Algebraic specification a step towards future software engineering

  • H. Partsch
Part I Algebraic Specification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 394)


The wide spectrum language CIP-L offers, among other concepts, algebraic abstract types for the formulation of formal problem specifications. This concept has been used for a real-life, large-scale application, viz. the (formal) specification of the (kernel of the) program transformation system CIP-S. From the general experiences with formal specification and the technical experiences in using CIP-L (with all its particularities) that were gained in this project, a number of objectives are derived, both for the design of practically usable languages based on the idea of algebraic specification and their support by appropriate tools as part of a comprehensive software engineering discipline.


Transformation Rule Type Scheme Type Definition Abstract Data Type Algebraic Specification 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Bartels et al. 81]
    Bartels, U., Olthoff, W., Raulefs, P.: APE: An expert system for automatic programming from abstract specifications of data types and algorithms. Fachbereich Informatik, Universität Kaiserslautern, MEMO SEKI-01-81, 1981Google Scholar
  2. [Bauer et al. 85]
    Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Geiselbrechtinger, F., Gnatz, R., Hangel, E., Hesse, W., Krieg-Brückner, B., Laut, A., Matzner, T., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: The Munich project CIP. Volume I: The wide spectrum language CIP-L. Lecture Notes in Computer Science 183, Berlin: Springer 1985Google Scholar
  3. [Bauer et al. 87]
    Bauer, F.L., Horsch, A., Möller, B., Partsch, H., Paukner, O., Pepper, P.: The Munich project CIP. Volume II: The transformation system CIP-S. Lecture Notes in Computer Science 292, Berlin: Springer 1987Google Scholar
  4. [Bauer et al. 88]
    Bauer, F.L., Möller, B., Partsch, H., Pepper, P: Programming by formal reasoning — an overview of the Munich CIP project. To appear in: IEEE Transactions on Software Engineering, 1988Google Scholar
  5. [Bergstra et al. 87]
    Bergstra, J.A., Heering, J., Klint P.: ASF — An algebraic specification formalism. Centre for Mathematics and Computer Science, Amsterdam, Technical Report CS-R8705, 1987Google Scholar
  6. [Bidoit, Choppy 85]
    Bidoit, M., Choppy, C.: ASSPEGIQUE: an integrated environment for algebraic specifications. Proc. International Joint Conference on Theory an Practice of Software Development, Berlin 1985. Lecture Notes in Computer Science 186, Berlin: Springer 1985, pp. 246–260Google Scholar
  7. [Bidoit et al. 87]
    Bidoit, M., Capy, F., Choppy, C., Choquet, N., Gresse, C., Kaplan, S., Schlienger, F., Voisin, F.: ASSPRO: an interactive and integrated programming environment. Technology and Science of Informatics 6:4, 259–278 (1987)Google Scholar
  8. [Bird 86]
    Bird, R.S.: An introduction to the theory of lists. Oxford University Computing Laboratory, Programming Research Group, Technical Monograph PRG-56, 1986Google Scholar
  9. [Botma 88]
    Botma, B.: AXLAB: A specification environment for algebraic types. Dept. of Computer Science, University of Nijmegen, Master thesis, 1988Google Scholar
  10. [Broy 83a]
    Broy, M.: Fixed Point theory for communication and concurrency. In: Bjørner, D. (ed.): IFIP TC2 Working Conference on Formal Description of Programming Concepts II, Garmisch-Partenkirchen, June 1982. Amsterdam: North-Holland, 1983Google Scholar
  11. [Broy 83b]
    Broy, M.: Applicative real time programming. In: Mason, R.E.A. (ed.): Information Processing 83. Proc. 9th IFIP World Computer Congress, Paris, Sept. 19–23, 1983. Amsterdam: North-Holland 1983, pp. 259–264Google Scholar
  12. [Broy 84]
    Broy, M.: Semantics of communicating processes. Information and Control 61, 202–246 (1984)CrossRefGoogle Scholar
  13. [Broy 85]
    Broy, M.: Specification and top down design of distributed systems. In: Ehrig, H., et al. (eds.): Formal methods and software development. Lecture Notes in Computer Science 186. Berlin: Springer 1985, pp. 4–28Google Scholar
  14. [Broy et al. 86]
    Broy, M., Möller, B., Pepper, P., Wirsing, M.: Algebraic implementations preserve program correctness. Science of Computer Programming 7, 35–53 (1986)CrossRefGoogle Scholar
  15. [Burstall, Goguen 80]
    Burstall, R.M., Goguen, J.A.: Semantics of CLEAR, a specification language. In: Bjørner, D. (ed.): Abstract software specifications. Lecture Notes in Computer Science 86, Berlin: Springer 1980, pp. 292–332Google Scholar
  16. [Ehler 85]
    Ehler, H.: Making formal specifications readable. Institut für Informatik, TU München, TUM-I8527, 1985Google Scholar
  17. [Ehrig et al. 83]
    Ehrig, H., Fey, W., Hansen, H.: ACT ONE — an algebraic specification language with two levels of semantics. Fachbereich 20, TU Berlin, Technical Report 83-03, 1983Google Scholar
  18. [Feijs et al. 87]
    Feijs, L.M.G., Jonkers, H.B.M, Obbink, J.H., Koymans, C.P.J., Renardel de Lavalette, G.R., Rodenburg, P.H.: A survey of the design language COLD. In: ESPRIT '86: Results and Achievements. Amsterdam: North-Holland 1987, pp. 631–644Google Scholar
  19. [Futatsugi et al. 85]
    Futatsugi, K., Goguen J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. Proc. 12th Ann. ACM Symp. on Principles of Programming Languages, ACM, 1985, pp. 52–66Google Scholar
  20. [Gaudel 85]
    Gaudel, M.C.: Toward structured algebraic specification. In: ESPRIT '85: Status Report of Continuing Work. Part I. Amsterdam: North-Holland, 1986, pp. 493–510Google Scholar
  21. [Gerhart et al. 80]
    Gerhart, S.L., Musser, D.R., Thompson, D.H., Baker, D.A., Bates, R.L., Erickson, R.W., London, R.L., Taylor, D.G., Wile, D.S.: An overview of AFFIRM: a specification and verification system. In: Lavington, S.H. (ed.): Information Processing 80, Amsterdam: North-Holland, 1980, pp. 343–347Google Scholar
  22. [Gerhart 81]
    Gerhart, S. (ed.): AFFIRM-type library. USC/Information Sciences Institute, Technical report 1981Google Scholar
  23. [Goguen, Tardo 77]
    Goguen, J.A., Tardo, J.: OBJ-0 preliminary users manual. Computer Science Department, University of California at Los Angeles, 1977Google Scholar
  24. [Goguen, Meseguer 81]
    Goguen, J., Meseguer, J.: OBJ-1, a study in executable algebraic formal specifications. SRI International, Technical Report 1981Google Scholar
  25. [Guttag, Horning 78]
    Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)CrossRefGoogle Scholar
  26. [Guttag, Horning 83]
    Guttag, J.V., Horning, J.J.: Preliminary Report on the LARCH shared language. Technical Report CSL 83-6, Xerox, Palo Alto, 1983Google Scholar
  27. [Heering, Klint 87]
    Heering, J., Klint, P.: A syntax definition formalism. In: ESPRIT '86: Results and Achievements. Amsterdam: North-Holland, 1987, pp. 619–630Google Scholar
  28. [Hußmann 85]
    Hußmann, H.: Rapid prototyping for algebraic specifications. RAP-System User's Manual. Fakultät für Mathematik und Informatik, Universität Passau, Report MIP-8504, 1985Google Scholar
  29. [Hußmann 87]
    Hußmann, H.: RAP-2 User Manual. Fachbereich Mathematik und Informatik, Universität Passau, Technischer Bericht 1987Google Scholar
  30. [Jonkers et al. 86]
    Jonkers, H.B.M., Koymans C.P.J., Renardel de Lavalette, G.R.: A semantic framework for the COLD-family of languages. Logic Group Preprint Series No. 9, Department of Philosophy, University of Utrecht, 1986Google Scholar
  31. [Krämer 87]
    Krämer, B.: SEGRAS — a formal language combining Petri nets and abstract data types for specifying distributed systems. Proc. 9th International Conference on Software Engineering, Monterey, Ca., 1987, pp. 116–125Google Scholar
  32. [Kühnel et al. 87]
    Kühnel, B., Partsch, H., Reinshagen, K.P.: Requirements Engineering — Versuch einer Begriffsklärung. Informatik-Spektrum 10:6, 334–335 (1987)Google Scholar
  33. [Lescanne 82]
    Lescanne, P.: Computer experiments with the REVE term rewriting system generator. Centre de Recherche en Informatique de Nancy, Technical Report, 1982Google Scholar
  34. [Leszcylowski, Wirsing 82]
    Leszcylowski, J., Wirsing, M.: A system for reasoning within and about algebraic specifications. In: Dezani-Ciancaglini, M., Montanari, U. (eds.): 5th Int. Symp. on Programming, Turin, Italy, 1982. Lecture Notes in Computer Science 137, Berlin: Springer 1982, pp. 257–282Google Scholar
  35. [London, Feather 82]
    London, P., Feather, M.S.: Implementing specification freedom. Science of Computer Programming 2, 91–131 (1982)CrossRefGoogle Scholar
  36. [Möller 86]
    Möller, B.: Algebraic specifications with higher-order operations. In: Meertens, L.G.L.T. (ed.): Program Specification and Transformation. Amsterdam: North-Holland 1986, pp. 367–392Google Scholar
  37. [Möller 87]
    Möller, B.: Higher-order algebraic specifications. Fachbereich Mathematik und Informatik, TU München, Habilitation thesis, 1987Google Scholar
  38. [Möller, Partsch 86]
    Möller, B., Partsch, H.: Formal specification of large-scale software: objectives, design decisions, and experiences in a concrete software project. In: Meertens, L.G.L.T. (ed.): Program Specification and Transformation. Amsterdam: North-Holland 1986Google Scholar
  39. [Neighbors 80]
    Neighbors, J.M.: Software construction using components. Ph. D. dissertation, Technical Report 160, University of California at Irvine, 1980Google Scholar
  40. [Parnas 72]
    Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Comm. ACM 15:12, 1053–1058 (1972)CrossRefGoogle Scholar
  41. [Partsch, Möller 87]
    Partsch, H., Möller, B.: Konstruktion korrekter Programme durch Transformation. Informatik-Spektrum 10:6, 309–323 (1987)Google Scholar
  42. [Pepper 84]
    Pepper, P.: A simple calculus for program transformations (inclusive of induction). Institut für Informatik, TU München, TUM-18409, 1984Google Scholar
  43. [Wile 86]
    Wile, D.S.: Local formalisms. In: Meertens, L.G.L.T. (ed.): Program Specification and Transformation. Amsterdam: North-Holland 1986Google Scholar
  44. [Wirsing 83]
    Wirsing, M.: A Specification Language. Fachbereich Mathematik und Informatik, TU München, Habilitation thesis, 1983Google Scholar
  45. [Wirsing et al. 83]
    Wirsing, M., Pepper, P., Partsch, H., Dosch, W., Broy, M.: On hierarchies of abstract data types. Acta Informatica 20, 1–33 (1983)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • H. Partsch
    • 1
  1. 1.KU NijmegenThe Netherlands

Personalised recommendations