Formalizing executable dynamic and forward slicing

This paper uses a projection theory of slicing to formalize the definition of executable dynamic and forward program slicing. Previous definitions, when given, have been operational, and previous descriptions have been algorithmic. The projection framework is used to provide a declarative formulation in terms of the different equivalences preserved by the different forms of slicing. The analysis of dynamic slicing reveals that the slicing criterion introduced by Korel and Laski contains three inter-woven criteria. It is shown how these three conceptually 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 slicing is more intricate that previous authors have claimed. Finally, the paper uses the projection theory to investigate theoretical properties of forward slicing. This is achieved by first re-formulating forward slicing to provide an executable forward slice. This definition allows for formal investigation of the relationship between forward and backward slicing. 1