Transformational meta program development

  • Bernd Krieg-Brückner
Part I. Development Models and Reusability
Part of the Lecture Notes in Computer Science book series (LNCS, volume 544)


The ESPRIT project PROgram development by SPECification and TRAnsformation is based on the CIP approach of TU München. Its most distinguishing feature is perhaps the use of algebraic specification and the transformational development paradigm not only for program but also for meta-program development, in fact to formalise the program development process itself. Transformation rules and their applicability conditions act as requirement specifications for transformation algorithms.

The extension of algebraic specification by higher order functions leads to a considerable increase in abstraction, avoiding much repetitive development effort. Homomorphic extension functionals, in particular, allow a concentration on the essential basic functions. Compared with classical functional programming, the algebraic properties allow reasoning about correctness and optimisation; the recursion schema of homomorphic extension acts as a program development strategy and as an induction schema for proofs.


Transformation Rule Abstract Syntax Concrete Syntax Recursion Schema Applicability Condition 
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. [1]
    Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Gnatz, R., Geiselbrechtinger, F., Hangel, E., Hesse, W., Krieg.-Brückner, B., Laut, A., Matzner, T.A., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: The Munich Project CIP, Vol. 1: The Wide Spectrum Language CIP-L. LNCS 183, Springer 1985.Google Scholar
  2. [2]
    Bauer, F.L., Ehler, H., Horsch, B., Möller, B., Partsch, H., Paukner, O., Pepper, P.,: The Munich Project CIP, Vol. 2: The Transformation System CIP-S. LNCS 292, Springer 1987.Google Scholar
  3. [3]
    Bauer, F.L., Möller, B., Partsch, H., Pepper, P.: Formal Program Construction by Stepwise Transformations — Computer-Aided Intuition-Guided Programming IEEE Trans. on SW Eng. 15:2 (1989) 165–180.Google Scholar
  4. [4]
    Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Springer 1982.Google Scholar
  5. [5]
    Bird, R.S.: Transformational Programming and the Paragraph Problem. Science of Computer Programming 6 (1986) 159–189.Google Scholar
  6. [6]
    Bird, R., Wadler, Ph.: Introduction to Functional Programming. Prentice Hall, 1988.Google Scholar
  7. [7]
    Bird, R.: Lectures on Constructive Functional Programming. in: Broy, M. (ed.): Constructive Methods in Computing Science. Springer (1989) 1–65.Google Scholar
  8. [8]
    Breu, M., Broy, M., Grünler, Th., Nickl, F.: PAnndA-S Semantics. PROSPECTRA Study Note M.2.1.S1-SN-1.4, Universität Passau, 1989.Google Scholar
  9. [9]
    Broy, M.: Equational Specification of Partial Higher Order Algebras. in: Broy, M. (ed.): Logic of Programming and Calculi of Discrete Design. NATO ASI Series, Vol. F36, Springer (1987) 185–241.Google Scholar
  10. [10]
    Broy, M.: Predicative Specification for Functional Programs Describing Communicating Networks. Information Processing Letters 25:2 (1987) 93–101.Google Scholar
  11. [11]
    Broy, M.: An Example for the Design of Distributed Systems in a Formal Setting: The Lift Problem. Universität Passau, Tech. Rep. MIP 8802 (1988).Google Scholar
  12. [12]
    Broy, M.: Towards a Design Methodology for Distributed Systems. in: Broy, M. (ed.): Constructive Methods in Computing Science. Springer (1989) 311–364.Google Scholar
  13. [13]
    Broy, M., Pepper, P., Wirsing, M.: On the Algebraic Definition of Programming Languages. ACM TOPLAS 9 (1987) 54–99.Google Scholar
  14. [14]
    Broy, M., Wirsing, M.: Partial Abstract Types. Acta Informatica 18 (1982) 47–64.Google Scholar
  15. [15]
    Feijs, L.M.G., Jonkers, H.B.M, Obbink, J.H., Koymans, P.P.J., Renardel de Lavalette, G.R., Rodenburg, P.M.: A Survey of the Design Language Cold. in: Proc. ESPRIT Conf. 86 (Results and Achievements). North Holland (1987) 631–644.Google Scholar
  16. [16]
    Ganzinger, H.: Ground Term Confluence in Parametric Conditional Equational Specifications. in: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M.(eds.): Proc. 4th Annual Symp. on Theoretical Aspects of Comp. Sci., Passau '87. LNCS 247 (1987) 286–298.Google Scholar
  17. [17]
    Ganzinger, H.: A Completion Procedure for Conditional Equations. Techn. Bericht No. 243, Fachbereich Informatik, Universität Dortmund, 1987 (to appear in J. Symb. Comp.)Google Scholar
  18. [18]
    Gordon, M., Milner, R., Wadsworth, Ch.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS 78.Google Scholar
  19. [19]
    Heckmann, R.: A Functional Language for the Specification of Complex Tree Transformations. in: Proc. European Symposium On Programming '88, LNCS 300 (1988).Google Scholar
  20. [20]
    Jähnichen, S., Hussain, F.A., Weber, M.: Program Development Using a Design Calculus. in: Rogers, M. W. (ed.): Results and Achievements, Proc. ESPRIT Conf. '86. North Holland (1987) 645–658.Google Scholar
  21. [21]
    Karlsen, E., Joergensen, J., Krieg-Brückner, B.: Functional in PAnndA-S. PROSPECTRA Study Note S.3.1.C1-SN-10.0, Dansk Datamatic Center, 1988.Google Scholar
  22. [22]
    Krieg-Brückner, B.: Systematic Transformation of Interface Specifications. in: Meertens, L.G.T.L. (ed.): Program Specification and Transformation, Proc. IFIP TC2 Working Conf. (Tölz '86). North Holland (1987) 269–291.Google Scholar
  23. [23]
    Krieg-Brückner, B.: Formalisation of Developments: An Algebraic Approach. in: Rogers, M. W. (ed.): Achievements and Impact. Proc. ESPRIT Conf. 87. North Holland (1987) 491–501.Google Scholar
  24. [24]
    Krieg-Brückner, B.: Algebraic Formalisation of Program Development by Transformation. in: Proc. European Symposium On Programming '88, LNCS 300 (1988) 34–48.Google Scholar
  25. [25]
    Krieg-Brückner, B.: The PROSPECTRA Methodology of Program Development. in: Zalewski (ed.): Proc. IFIP/IFAC Working Conf. on HW and SW for Real Time Process Control (Warsaw). North Holland (1988) 257–271.Google Scholar
  26. [26]
    Krieg-Brückner, B.: Algebraic Specification and Functionals for Transformational Program and Meta Program Development. in Díaz, J., Orejas, F. (eds.): Proc. TAPSOFT '89 (Barcelona), Vol. 2. LNCS 352 (1989) 36–59.Google Scholar
  27. [27]
    Krieg-Brückner, B.: Algebraic Specification with Functionals in Program Development by Transformation. in: ESPRIT '89, Proc. 6th Annual ESPRIT Conference, Kluwer Acad. Publ. (1989) 302–320.Google Scholar
  28. [28]
    Krieg-Brückner, B. (ed.): PROgram development by SPECification and TRAnsformation: Part I: The PROSPECTRA Methodology, Part II: The PROSPECTRA Language Family, Part III: The PROSPECTRA System. PROSPECTRA Reports M.1.1.S3-R-55.1,-56.1,-57.1. Universität Bremen, 1990. (to be published).Google Scholar
  29. [29]
    Luckham, D.C., von Henke, F.W., Krieg-Brückner, B., Owe, O.: Anna, a Language for Annotating Ada Programs, Reference Manual. LNCS 260, Springer (1987).Google Scholar
  30. [30]
    Möller, B.: Algebraic Specification with Higher Order Operators. in: Meertens, L.G.T.L. (ed.): Program Specification and Transformation, Proc. IFIP TC2 Working Conf. (Tölz '86). North Holland (1987) 367–398.Google Scholar
  31. [31]
    Nickl, F., Broy, M., Breu, M., Dederichs, F., Grünler, Th.: Towards a Semantics of Higher Order Specifications in PAnndA-S. PROSPECTRA Study Note M.2.1.S1-SN-2.0, Universität Passau, 1988.Google Scholar
  32. [32]
    Owe. O.: An Approach to Program Reasoning Based on a First Order Logic for Partial Functions. Research Report No. 89, Institute of Informatics, University of Oslo, 1985.Google Scholar
  33. [33]
    Partsch, H., Steinbrüggen, R.: Program Transformation Systems. ACM Computing Surveys 15 (1983) 199–236.Google Scholar
  34. [34]
    Reference Manual for the Ada Programming Language. ANSI/MIL.STD 1815A. US Government Printing Office, 1983. Also in: Rogers, M. W. (ed.): Ada: Language, compilers and Bibliography. Ada Companion Series, Cambridge University Press, 1984.Google Scholar
  35. [35]
    Reps., Teitelbaum: The Synthesizer Generator. Springer, 1988.Google Scholar
  36. [36]
    Reps., Teitelbaum: The Synthesizer Generator; Reference Manual. Springer, 1988.Google Scholar
  37. [37]
    Sintzoff, M.: Expressing Program Developments in a Design Calculus. in: Broy, M. (ed.): Logic of Programming and Calculi of Discrete Design. NATO ASI Series, Vol. F36, Springer (1987) 343–365.Google Scholar
  38. [38]
    Smith, D.R.: Top-Down Synthesis of Divide-and-Conquer Algorithms. Artificial Intelligence 27:1 (1985) 43–95.Google Scholar
  39. [39]
    Steinbrüggen, R.: Program Development using Transformational Expressions. Rep. TUM-I8206, Institut für Informatik, TU München, 1982.Google Scholar
  40. [40]
    Traynor, O.: The Methodology of Verification in PROSPECTRA. PROSPECTRA Study Note S.3.4.-SN-19.0, University of Strathclyde, 1989.Google Scholar
  41. [41]
    Traynor, O.: The PROSPECTRA Proof Editor. PROSPECTRA Study Note S.3.4.-SN-15.2, University of Strathclyde, 1989.Google Scholar
  42. [42]
    von Henke, F.W.: An Algebraic Approach to Data Types, Program Verification and Program Synthesis. in: Mazurkiewicz, A. (ed.): Mathematical Foundations of Computer Science 1976. LNCS 45 (1976) 330–336.Google Scholar
  43. [43]
    Wile, D. S.: Program Developments: Formal Explanations of Implementations. CACM 26: 11 (1983) 902–911. also in: Agresti, W. A. (ed.): New Paradigms for Software Development. IEEE Computer Society Press/North Holland (1986) 239–248.Google Scholar
  44. [44]
    Wile, D. S.: Organizing Programming Knowledge into Syntax Directed Experts. Proc. Int'l Workshop on Advanced Programming Environments (Trondheim). LNCS 244 (1986) 551–565.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Bernd Krieg-Brückner
    • 1
  1. 1.FB3 Mathematik und InformatikUniversität BremenBremen 33FR Germany

Personalised recommendations