Program analysis by formal transformation

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Ward, Martin
dc.date.accessioned 2005-09-05T19:59:12Z
dc.date.available 2005-09-05T19:59:12Z
dc.date.issued 2005-09-05T19:59:12Z
dc.identifier.citation Ward, M. (1996) Program analysis by formal transformation. The Computer Journal, 39 (7), pp.598-618.
dc.identifier.other IR/2005/26
dc.identifier.uri http://hdl.handle.net/2086/49
dc.description.abstract This paper treats Knuth and Szwarcfiter’s topological sorting program, presented in their paper “A structured program to generate all topological sorting arrangements” (Knuth and Szwarcfiter 1974), as a case study for the analysis of a program by formal transformations. This algorithm was selected for the case study because it is a particularly challenging program for any reverse engineering method. Besides a complex control flow, the program uses arrays to represent various linked lists and sets, which are manipulated in various “ingenious” ways so as to squeeze the last ounce of performance from the algorithm. Our aim is to manipulate the program, using semantics-preserving operations, to produce an abstract specification. The transformations are carried out in the WSL language, a “wide spectrum language” which includes both low-level program operations and high level specifications, and which has been specifically designed to be easy to transform. en
dc.description.sponsorship Supported by an EPSRC project: "A proof theory for program refinement and equivalence: extensions". en
dc.format.extent 474366 bytes
dc.format.extent 554137 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1996-13 en
dc.subject EPSRC
dc.title Program analysis by formal transformation en
dc.type Article en
dc.identifier.doi doi:10.1093/comjnl/39.7.598
dc.researchgroup Software Technology Research Laboratory (STRL)


Files in this item

This item appears in the following Collection(s)

Show simple item record