The semantics of program slicing and program integration

A slice of a program with respect to a program point p and variable x consists of all statements of the program that might affect the value of x at point p. Slices can be extracted particularly easily from a program representation called a program dependence graph, originally introduced as an intermediate program representation for performing optimizing, vectorizing, and parallelizing transformations. Such slices are of a slightly restricted form: rather than permitting a program to be sliced with respect to program point p and an arbitrary variable, a slice must be taken with respect to a variable that is defined at or used at p. This paper concerns the relationship between the execution behavior of a program and the execution behavior of its slices. Our main results about slicing are those stated as the Slicing Theorem and the Termination Theorem. The Slicing Theorem demonstrates that a slice captures a portion of a program's behavior in the sense that, for any initial state on which the program halts, the program and the slice compute the same sequence of values for each element of the slice. The Termination Theorem demonstrates that if a program is decomposed into (two or more) slices, the program halts on any state for which all the slices halt. These results are then used to provide semantic justification for a program-integration algorithm of Horwitz, Prins, and Reps.