Abstract
In the methodology for the development of correct softwareby transformation, each development step corresponds to the application of a preconceived transformation rule or method. The framework is generic with respect to an object language and permits the verification of semantic correctness. Elementary transformation rules incorporate a powerful notion of matching that allows abstraction to rule schemata. Higher-order rules are the elements of a tactical calculus with a number of desirable algebraic properties. This is the basis for a formalisation of transformational developments, for generalisation of concrete developments to tactical methods, and for a refinement of methods to efficient transformation scripts. Thus reusability of the development process is achieved and general, correct development methods can be established and refined into efficient tactical programs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.C. Backhouse, P.J. de Bruin, G. Malcolm, E. Voermans, J. van der Woude. Relational Catamorphisms. In B. Möller (eds.): Proc. IFIP TC2 Working Conference on Constructing Programs from Specifications, pp. 278–309, 1991.
L. Bachmair. Canonical Equational Proofs. 1991.
R.S. Bird, O. de Moor. Solving Optimizations with Catamorphisms. LNCS 669, pp. 45–67, 1992.
M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hussmann, D. Nazareth, F. Regensburger, K. Stølen. The Requirement and Design Specification Language SPECTRUM: An Informal Introduction. Technical Report TUM-19311 (19312), Institut für Informatik, Technische Universität München, 1993.
F.L. Bauer, H. Wössner. Algorithmic Language and Program Development. Springer 1982.
F.L. Bauer, R. Berghammer, M. Broy, W. Dosch, R. Gnatz, F. Geiselbrechtinger, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T.A. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, H. Wössner. The Munich Project CIP, Vol. 1: The Wide Spectrum Language CIP-L. LNCS 183, 1985.
F.L. Bauer, H. Ehler, B. Horsch, B. Möller, H. Partsch, O. Paukner, P. Pepper. The Munich Project CIP, Vol. 2: The Transformation System CIP-S. LNCS 292, 1987.
J. Farres-Cassals. Verification in ASL and Related Specification Languages. Phd Thesis, LFCS Report ECS-LFCS-92-220, Dept. of Computer Science, University of Edinburgh, 1992.
J.A. Goguen, R.M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, vol. 39, No. 1, pp. 95–146, 1992.
B. Hoffmann, B. Krieg-Brückner (eds.). Program Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680, 1993.
G. Huet, B. Lang (eds.). Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica 11, pp. 30–55, 1978.
J.-P. Jouannaud, E. Kirchner. Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Compt. 15, pp. 1155–1194, 1986.
B. Krieg-Brückner. Algebraic Specification and Functional for Transformational Program and Meta-Program Development. In J. Diaz, F. Orejas (eds.): Proc. TAPSOFT 89, LNCS 352, pp.35–59, 1989.
B. Krieg-Brückner (Hrsg.). Programmentwicklung durch Spezifikation und Transformation — Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software). Technical Report 1/94, Universität Bremen, 1994.
B. Krieg-Brückner (Hrsg.). Programmentwicklung durch Spezifikation und Transformation — Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software); Band 2. Technical Report 10/94, Universität Bremen, 1994.
B. Krieg-Brückner, E.W. Karlsen, J. Liu, O Traynor. The PROSPECTRA Methodology and System: Uniform Transformational (Meta-) Development. in: S. Prehn, W.J. Toetenel (eds.): VDM'91, Formal Software Development Methods; Vol. 2: Tutorials. LNCS 552, pp. 363–397, 1991.
J.W. Klop. Term Rewriting Systems. S. Abramsky, Dov M. Gabbay, T.S.E. Maibaum (eds): Handbook of Logic in Computer Science, Vol 2, Chapter 1. Oxford Science Publications, pp. 1–116, 1992.
B. Krieg-Brückner, W. Menzel, W. (eds.), W. Reif, H. Ruess, Th. Santen, D. Schwier, G. Schellhorn, K. Stenzel, W. Stephan. System Architecture Framework for KORSO. in [KB94a].
Kolyang, B. Wolff, J. Liu. Transformational Development of the LEX Example. in [KB94b].
J. Liu. A Semantic Basis for Logic-Independent Transformations. In F. Orejas (eds.): Proc. 9th WADT-COMPASS Workshop, LNCS 785, pp. 268–279, 1994, also in [KB94a].
J. Liu. Higher-Order Structured Presentation in a Logical Framework. Dissertation, Universität Bremen, 1994.
J. Liu. Formal Correctness Proof of a Transformation Rule in LEGO: Split of Postcondition, Technical Report 95, Universität Bremen, 1995.
B. Möller. Relations as a Program Development Language. In B. Möller (eds.): Proc. IFIP TC2 Working Conference on Constructing Programs from Specifications. pp. 353–376, 1991.
V. van Oostrom. Lambda Calculus with Patterns. Dept. of Mathematics and Computer Science, Vrije Universiteit, Technical Report, 1990.
P. Pepper, M. Wirsing. A Method for the Development of Correct Software (in this volume).
H. Shi. Extended Matching and Application to Program Transformation. Dissertation, Universität Bremen, 1994.
D. Sannella, A. Tarlecki. Towards formal development of programs from algebraic specifications: implementations revisited. In H. Ehrig et al.(eds.): Proc. TAPSOFT 87, LNCS 249, pp. 96–110, 1987.
D. Sannella, A. Tarlecki. Specification in an arbitrary institution. Information and Computation 76, pp. 165–210, 1988.
H. Shi, B. Wolff. A Finitary Matching Algorithm for Constructor Based Theories. in [KB94a].
M. Weber. Definition and Basic Properties of the Deva Meta-Calculus. Formal Aspects of Computing 5 (5), pp. 391–431, 1993.
B. Wolff. Proving Transformations in Isabelle. in [KB94b].
B. Wolff, H. Shi. A Calculus of Transformation. in [KB94b].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Krieg-Brückner, B., Liu, J., Shi, H., Wolff, B. (1995). Towards correct, efficient and reusable transformational developments. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015467
Download citation
DOI: https://doi.org/10.1007/BFb0015467
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60589-8
Online ISBN: 978-3-540-47802-7
eBook Packages: Springer Book Archive