Recursion removal/introduction by formal transformation: an aid to program development and program comprehension

De Montfort University Open Research Archive

Show simple item record Ward, Martin Bennett, Keith H. 2005-09-05T19:30:31Z 2005-09-05T19:30:31Z 1999
dc.identifier.citation Ward, M.P. and Bennett, K.H., Recursion removal/introduction by formal transformation: an aid to program development and program comprehension, In: The computer journal, vol.42, no.8, 1999, pp 650-673 en
dc.identifier.issn 0010-4620
dc.identifier.other IR/2005/21
dc.description Peer-reviewed. received 16th March 1999; accepted 8th September 1999 en
dc.description.abstract The transformation of a recursive program to an iterative equivalent is a fundamental operation in Computer Science. In the reverse direction, the task of reverse engineering (analysing a given program in order to determine its specification) can be greatly ameliorated if the program can be re-expressed in a suitable recursive form. But the existing recursion removal transformations, such as the techniques discussed by Knuth [1] and Bird [2], can only be applied in the reverse direction if the source program happens to match the structure produced by a particular recursion removal operation. In this paper we describe a much more powerful recursion removal and introduction operation which describes its source and target in the form of an action system (a collection of labels and calls to labels). A simple, mechanical, restructuring operation can be applied to a great many iterative programs which will put them in a suitable form for recursion introduction. Our transformation generates strictly more iterative versions than the standard methods, including those of Knuth and Bird [1,2]. With the aid of this theorem we prove a (somewhat counterintuitive) result for programs that contain sequences of two or more recursive calls: under a reasonable commutativity condition, “depth-first” execution is more general than “breadth-first” execution. In “depth-first” execution, the execution of each recursive call is completed, including all sub-calls, before execution of the next call is started. In “breadth-first” execution, each recursive call in the sequence is partially executed but any sub-calls are temporarily postponed. This result means that any breadth-first program can be reimplemented as a corresponding depth-first program, but the converse does not hold. We also treat the case of “random-first” execution, where the execution order is implementation dependent. For the more restricted domain of tree searching we show that breadth first search is the most general form. We also give two examples of recursion introduction as an aid to formal reverse engineering. en
dc.format.extent 377167 bytes
dc.format.extent 399555 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.publisher Oxford University Press en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1999/10 en
dc.subject recursion en
dc.subject formal methods en
dc.subject reverse engineering en
dc.subject re-engineering en
dc.subject WSL en
dc.subject wide spectrum language en
dc.subject refinement en
dc.subject program comprehension en
dc.title Recursion removal/introduction by formal transformation: an aid to program development and program comprehension en
dc.type Article en
dc.researchgroup Software Technology Research Laboratory (STRL)

Files in this item

This item appears in the following Collection(s)

Show simple item record