Abstract
The methodology of program development by transformation, as it is represented in the PROSPECTRA project ([KKLT 91], [HK 93]), for example, integrates the tasks of program construction and verification. Both are carried out as fundamental parts of the development process. The implementor starts with a formal requirements specification defining the essential requirements in the interface that a software system or component must satisfy. This initial specification is then gradually refined into an optimised, executable, possibly machine-oriented specification. Refinement is achieved by stepwise application of pre-conceived, correctness-preserving transformations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
N. Dershowitz, J-P. Jouannaud: Rewrite Systems. In: Handbook of Theoretical Computer Science. Elsevier, 1990.
R. Harper, F. Honsell, G. Plotkin. A Framework for Defining Logics. Proc. 2nd IEEE Symp. on Logic in Computer Science, Cornell, 1987,194–204.
B. Krieg-Brückner, B. Hoffmann (eds.): Program development by Specification and Transformation: The PROSPECTRA Methodology, Language Family, and System. LNCS 680,1993.
G. Huet, B. Lang: Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica, 11,1978.
R. Harper, D. Sannella, A. Tarlecki. Structure and Representation in LF. LFCS Report ECS-LFCS-89-75, Dept. of Computer Science, Uni. of Edinburgh.
Krieg-Brückner, B.: Algebraic Specification and Functional for Transformational Program and Meta Program Devlopment. in Diaz, J., Orejas, F. (eds): Proc. TAPSOFT’89 (Barcelona), Vol. 2. LNCS 352,1989,36–59.
Krieg-Briickner, B., Karlsen, E., Liu, J., Traynor, O.: The PROSPECTRA Methodology and System: A Unified Development Framework. In Proc. VDM ’91, Springer Verlag, LNCS 552,1991, 361–397.
J.W. Klop: Term Rewriting Systems. Appeared in: S. Abramski, Dov. M. Gabbay, T.S.E. Maibaum (eds): Handbook of Logic in Computer Science, Chapter 1. Oxford Science Publications, 1992.
J. Liu: A Semantic Basis for Logic-Independent Transformation. Korso Report, Universität Bremen, 1993.
Sannella, D., Tarlecki, A.: Extended-ML: an Institution Independent Framework for Formal Program Development LNCS 240, (1986).
Shi, H., Wolff, B.: Second-Order Matching with Matching Combinators. KORSO Report, FB3 Informatik, Universität Bremen, 1993.
Wolff, B., Shi, H.: Towards a Meta-Language for Reusable Transformational Developments. KORSO Report, FB3 Informatik, Universität Bremen, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krieg-Brückner, B., Liu, J., Wolff, B., Shi, H. (1993). Towards Correctness, Efficiency and Reusability of Transformational Developments. In: Reichel, H. (eds) Informatik — Wirtschaft — Gesellschaft. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-78486-6_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-78486-6_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57192-6
Online ISBN: 978-3-642-78486-6
eBook Packages: Springer Book Archive