Abstract
A style of program construction which consists of alternating successive steps of specification, derivation and verification is demonstrated by a simple example. All steps are carried out within a purely axiomatic framework. The demonstration example is the evaluation of expressions in reverse Polish notation. Expressions given in the form of trees can easily be evaluated by a function specified by a straightforward recursive function declaration the correctness of which is obvious and therefore can be taken as initial specification. The recursive function declaration is transformed to one working on reverse Polish notation that is derived from the trees by postorder tree traversal. Constructive proofs are given that show the correctness of the produced program.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Berghammer R., Ehler H., Zierer H.: Towards an algebraic specification of code generation. Report TUM-18707, Institut für Informatik, Technische Universität München (1987)
Bauer F. L., Wössner H.: Algorithmische Sprache und Programmentwicklung. Springer: Berlin-Heidelberg-New York (1981). English translation: Algorithmic language and program development. Springer: Berlin-Heidelberg-New York (1982)
Broy M.: Predicative specification for functional programs describing communicating networks. Information Processing Letters 25, 1987, 93–101
Geser A., Hußmann H.: Rapid prototyping for algebraic specifications — Examples of the use of the RAP system. Report MIP-8517, Fakultät für Mathematik und Informatik, Universität Passau (1985)
George Ch.: Practical aspects of development. RAISE Document, STC 1988
Hußmann H.: Unification in conditional-equational theories. Proc. EUROCAL '85, Springer LNCS 204 543–553 (1985). Also: Report MIP-8502, Fakultät für Mathematik und Informatik, Universität Passau (1985)
Hehner E.C.R.: Predicative specification Part I+II. CACM 27:2 (1984) 134–151
McCarthy J., Painter J.: Correctness of a compiler for arithmetic expressions. In: Schwartz J.T. (ed.): Mathematical aspects of computer science. Proc. of symposia in applied mathematics 19, 33–41 (1967)
Samelson K., Bauer F. L.: Sequentielle Formelübersetzung. Elektronische Rechenanlagen 1, 176–182 (1959). English translation: Sequential formula translation. CACM 3, 76–83 (1960)
Wirsing M., Pepper P., Partsch H., Dosch W., Broy M.: On hierarchies of abstract data types. Acta Informatica 20, 1983, 1–33
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Broy, M. (1991). Deductive program development: Evaluation in reverse Polish notation as an example. In: Broy, M., Wirsing, M. (eds) Methods of Programming. Lecture Notes in Computer Science, vol 544. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018270
Download citation
DOI: https://doi.org/10.1007/BFb0018270
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54576-7
Online ISBN: 978-3-540-38491-5
eBook Packages: Springer Book Archive