The Semantics of Program Slicing
Thomas Reps, Wuu Yang · 1988
... This paper concerns the relationship between the execution behavior of a program and the execution behavior of its slices. Our main results 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