Slicing as a program transformation

The aim of this article is to provide a unified mathematical framework for program slicing which places all slicing work for sequential programs on a sound theoretical foundation. The main advantage to a mathematical approach is that it is not tied to a particular representation. In fact the mathematics provides a sound basis for any particular representation. We use the WSL (wide-spectrum language) program transformation theory as our framework. Within this framework we define a new semantic relation, semirefinement, which lies between semantic equivalence and semantic refinement. Combining this semantic relation, a,syntactic relation (called reduction), and WSL's remove statement, we can give mathematical definitions for backwards slicing, conditioned slicing, static and dynamic slicing, and semantic slicing as program transformations in the WSL transformation theory. A novel technique of "encoding" operational semantics within a denotational semantics allows the framework to handle "operational slicing". The theory also enables the concept of slicing to be applied to nondeterministic programs. These transformations are implemented in the industry-strength FermaT transformation system.