Abstract
In this paper we briefly introduce a Wide Spectrum Language and its transformation theory and describe a recent success of the theory: a general recursion removal theorem. Recursion removal often forms an important step in the systematic development of an algorithm from a formal specification. We use semantic-preserving transformations to carry out such developments and the theorem proves the correctness of many different classes of recursion removal. This theorem includes as special cases the two techniques discussed by Knuth [13] and Bird [7]. We describe some applications of the theorem to cascade recursion, binary cascade recursion, Gray codes, and an inverse engineering problem.
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
W. Ackermann, “Zum Hilbertschen Aufbau der reellen Zahlen,” Math. Ann. 99 (1928), 118–133.
J. Arsac, “Transformation of Recursive Procedures,” in Tools and Notations for Program Construction, D. Neel, ed., Cambridge University Press, Cambridge, 1982, 211–265.
J. Arsac, “Syntactic Source to Source Program Transformations and Program Manipulation,” Comm. ACM 22 (Jan., 1982 ), 43–54.
R. J. R. Back, Correctness Preserving Program Refinements, Mathematical Centre Tracts#131, Mathematisch Centrum, 1980.
F. L. Bauer, B. Moller, H. Partsch und P. Pepper, “Formal Construction by Transformation—Computer Aided Intuition Guided Programming,” IEEE Trans. Software Eng. 15 (Feb., 1989 ).
F. L. Bauer und H. Wossner, Algorithmic Language and Program Development, Springer-Verlag, New York–Heidelberg–Berlin, 1982.
R. Bird, “Notes on Recursion Removal,” Comm. ACM 20 (June, 1977 ), 434–439.
R. Bird, “Lectures on Constructive Functional Programming,” Oxford University, Technical Monograph PRG-69, Sept., 1988.
P. T. Breuer, K. Lano und J. Bowen, “Understanding Programs through Formal Methods,” Oxford University, Programming Research Group, 9 Apr., 1991.
T. Bull, “An Introduction to the WSL Program Transformer,” Conference on Software Maintenance 1990, San Diago (Nov. 26th-29th, 1990 ).
B. A. Davey und H. A. Priestley, Introduction to Lattices and Order, Cambridge University Press, Cambridge, 1990.
E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ, 1976.
D. E. Knuth, “Structured Programming with the GOTO Statement,” Comput. Surveys 6 (1974), 261–301.
C. Morgan, Programming from Specifications, Prentice-Hall, Englewood Cliffs, NJ, 1990.
C. Morgan und K. Robinson, “Specification Statements and Refinements,” IBM J. Res. Develop. 31 (1987).
C. C. Morgan, “The Specification Statement,” ACM TOPLAS 10 (1988), 403–419.
C. C. Morgan, K. Robinson und Paul Gardiner, “On the Refinement Calculus,” Oxford University, Technical Monograph PRG-70, Oct., 1988.
E. L. Post, “Formal Reduction of the General Combinatorial Decision Problem,” Amer. J. Math. (1943).
D. Taylor, “An Alternative to Current Looping Syntax,” SIGPLAN Notices 19 (Dec., 1984), 48–53.
M. Ward, “Proving Program Refinements and Transformations,” Oxford University, DPhil Thesis, 1989.
M. Ward, “Derivation of a Sorting Algorithm,” Durham University, Technical Report, 1990.
M. Ward, “Specifications and Programs in a Wide Spectrum Language,” Durham University, Technical Report, 1990.
M. Ward, “A Definition of Abstraction,” University of Durham Technical Report, 1990.
M. Ward, “A Recursion Removal Theorem - Proof and Applications,” University of Durham, Technical Report, 1991.
M. Ward, “The Largest True Square Problem—An Exercise in the Derivation of an Algorithm,” Durham University, Technical Report, Apr., 1990.
M. Ward, “The Schorr-Waite Graph Marking Algorithm An Exercise in the Derivation of an Algorithm,” Durham University, Technical Report, Apr., 1990.
M. Ward, “Abstracting a Specification from Code,” Submitted to Journal of Software Maintenance and Management, Aug., 1991.
M. Ward, F. W. Calliss und M. Munro, “The Maintainer’s Assistant,” Conference on Software Maintenance 1989, Miami Florida(Oct. 16th-19th, 1989 ).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 Springer-Verlag London
About this paper
Cite this paper
Ward, M. (1992). A Recursion Removal Theorem. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds) 5th Refinement Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3550-0_4
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3550-0_4
Publisher Name: Springer, London
Print ISBN: 978-3-540-19752-2
Online ISBN: 978-1-4471-3550-0
eBook Packages: Springer Book Archive