Abstract
A methodology for PROgram development by SPECification and TRAnsformation is described. Formal requirement specifications are the basis for constructing correct and efficient programs by gradual transformation.
A uniform treatment of algebraic specification is presented to formalise data, programs, transformation rules, in fact the program development process itself. It is shown by example that the development of meta programs, for example an efficient transformation algorithm incorporating the effect of a set of transformation rules, is analogous to program development: the transformation rules act as specifications for the transformation algorithms, and the negation of their applicability conditions as development goals.
The paper focusses on the combination of functional programming and algebraic specification and reasoning, leading to a considerably higher degree of abstraction, avoiding much repetitive development effort, the use of homomorphic extension functionals, homomorphic properties for reasoning about correctness and optimisation, and the recursion schema of homomorphic extension as a program development strategy and as an induction schema for proofs.
The research reported herein has been partially funded by the Commission of the European Communities under the ESPRIT Programme, Project #390, PROSPECTRA (PROgram development by SPECification and TRAnsformation)
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Krieg-Brückner, B., Hoffmann, B., Ganzinger, H., Broy, M., Wilhelm, R., Möncke, U., Weisgerber, B., McGettrick, A.D., Campbell, I.G., Winterstein, G.: PROgram Development by SPECification and TRAnsformation. in: Rogers, M. W. (ed.): Results and Achievements, Proc. ESPRIT Conf. '86. North Holland (1987) 301–312.
Krieg-Brückner, B.: Integration of Program Construction and Verification: the PROSPECTRA Project. in: Habermann, N., Montanari, U. (eds.): Innovative Software Factories and Ada. Proc. CRAI Int'l Spring Conf. '86. LNCS 275 (1987) 173–194.
Bauer, F.L.: Program Development by Stepwise Transformations — The Project CIP. in: Bauer, F. L., Broy, M. (eds.): Program Construction. LNCS 69, Springer 1979.
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.
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.
Partsch, H., Steinbrüggen, R.: Program Transformation Systems. ACM Computing Surveys 15 (1983) 199–236.
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.
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).
Bertling, H., Ganzinger, H.: A Structure Editor Based on Term Rewriting. in: Proc. 2nd ESPRIT Technical Week, Brussels (1985) 455–466.
Möncke, U., Weisgerber, B., Wilhelm, R.: Generative Support for Transformational Programming. in: Proc. 2nd ESPRIT Technical Week, Brussels (1985) 511–528.
Heckmann, R.: A Functional Language for the Specification of Complex Tree Transformations. in: Proc. European Symposium on Programming '88, LNCS 300 (1988).
Broy, M., Pepper, P., Wirsing, M.: On the Algebraic Definition of Programming Languages. ACM TOPLAS 9 (1987) 54–99.
Broy, M., Wirsing, M.: Partial Abstract Types. Acta Informatica 18 (1982) 47–64.
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.
Krieg-Brückner, B.: Transformation of Interface Specifications. in: Kreowski, H.-J. (ed.): Recent Trends in Data Type Specification. Informatik Fachberichte 116, Springer 1985, 156–170.
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.
Broy, M., Möller, B., Pepper, P., Wirsing, M.: Algebraic Implementations Preserve Program Correctness. Science of Computer Programming 7 (1986) 35–53.
Breu, M., Broy, M., Grünler, Th., Nickl, F.: PAnndA-S Semantics. PROSPECTRA Study Note M.2.1.S1-SN-1.3, Universität Passau, 1988.
Kahrs, S.: PAnndA-S Standard Types. PROSPECTRA Study Note M.1.1.S1-SN-11.2, Universität Bremen, 1986.
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.
Ganzinger, H.: A Completion Procedure for Conditional Equations. Techn. Bericht No. 243, Fachbereich Informatik, Universität Dortmund, 1987 (to appear in J. Symb. Comp.)
Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Springer 1982.
Kahrs, S.: From Constructive Specifications to Algorithmic Specifications. PROSPECTRA Study Note M.3.1.S1-SN-1.2, Universität Bremen, 1986.
Pepper, P.: A Simple Calculus of Program Transformations (Inclusive of Induction). Science of Computer Programming 9: 3 (1987) 221–262.
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.
Krieg-Brückner, B.: Algebraic Formalisation of Program Development by Transformation. in: Proc. European Symposium On Programming '88, LNCS 300 (1988) 34–48.
Broy, M.: Predicative Specification for Functional Programs Describing Communicating Networks. Information Processing Letters 25:2 (1987) 93–101.
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).
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.
Steinbrüggen, R..: Program Development using Transformational Expressions. Rep. TUM-I8206, Institut für Informatik, TU München, 1982.
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.
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.
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.
Bird, R.S.: Transformational Programming and the Paragraph Problem. Science of Computer Programming 6 (1986) 159–189.
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.
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.
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.
Gordon, M., Milner, R., Wadsworth, Ch.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS 78.
Smith, D.R.: Top-Down Synthesis of Divide-and-Conquer Algorithms. Artificial Intelligence 27:1 (1985) 43–95.
Wile, D. S.: Organizing Programming Knowledge into Syntax Directed Experts. Proc. Int'l Workshop on Advanced Programming Environments (Trondheim). LNCS 244 (1986) 551–565.
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.
Bird, R., Wadler, Ph.: Introduction to Functional Programming. Prentice Hall 1988.
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.
Karlsen, E., Joergensen, J., Krieg-Brückner, B.: Functionals in PAnndA-S. PROSPECTRA Study Note S.3.1.C1-SN-10.0, Dansk Datamatic Center, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krieg-Brückner, B. (1989). Algebraic specification and functionals for transformational program and meta program development. In: Díaz, J., Orejas, F. (eds) TAPSOFT '89. TAPSOFT 1989. Lecture Notes in Computer Science, vol 352. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50940-2_26
Download citation
DOI: https://doi.org/10.1007/3-540-50940-2_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50940-0
Online ISBN: 978-3-540-46118-0
eBook Packages: Springer Book Archive