© 1996 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Program Analysis by Formal Transformation
Computer Science Department, University of Durham Science Laboratories, South Rd, Durham DH1 3LE, UK. Email: Martin.Ward{at}durham.ac.uk
This paper treats Knuth and Szwarcfiter's topological sorting program 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.
Received July 18, 1995. revised November 4, 1996.
* Computer Science Department, University of Durham Science Laboratories, South Road, Durham DH1 3LE, UK Email: Martin.Ward{at}durham.ac.uk