Formalizing Executable Dynamic and Forward Slicing

This paper uses a projection theory of slicing to formal-ize the definition of executable dynamic and forward pro-gram slicing. Previous definitions, when given, have been operational, and previous descriptions have been algorith-mic. The projection framework is used to provide a declar-ative formulation in terms of the different equivalences pre-served by the different forms of slicing. The analysis of dynamic slicing reveals that the slic-ing criterion introduced by Korel and Laski contains three inter-woven criteria. It is shown how these three conceptu-ally distinct criteria can be disentangled to reveal two new criteria. The analysis of dynamic slicing also reveals that the subsumes relationship between static and dynamic slic-ing is more intricate that previous authors have claimed. Finally, the paper uses the projection theory to inves-tigate theoretical properties of forward slicing. This is achieved by first re-formulating forward slicing to provide an executable forward slice. This definition allows for for-mal investigation of the relationship between forward and backward slicing. 1