A Formal Method for Program Slicing

Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular computation. Based on modular monadic semantics of a programming language, this paper presents a new formal method for slicing, called modular monadic slicing, by abstracting the computation of slicing as a slice monad transformer. With the use of slice transformer, the feature of program slicing can be combined in a modular way into semantic descriptions of the program analyzed. According to these, this paper gives both monadic dynamic and static slicing algorithms. They compute program slices directly on abstract syntax, without the needs to explicitly construct intermediate structures such as dependence graphs, or to record an execution history in dynamic slicing algorithm.