PROGRAM ANALYSIS BY FORMAL TRANSFORMATION

This paper treats Knuth and Szwarcfiter's topological sorting program as a case study for the analysis of a program by formal transformation s. This algorithm was selected for the case study because it is a part icularly challenging program for any reverse engineering method, Besid es a complex control how, the program uses arrays to represent various linked lists and sets, which are manipulated in various 'ingenious' w ays so as to squeeze the last ounce of performance from the algorithm. Our aim is to manipulate the program, using semantics-preserving oper ations, to produce an abstract specification, The transformations are carried out in the WSL language, a 'wide spectrum language' which incl udes both low-level program operations and high level specifications, and which has been specifically designed to be easy to transform.