Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular computation. The current slicing methods, however, are singular （mainly based on a program or...Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular computation. The current slicing methods, however, are singular （mainly based on a program or system dependence graph）, and lack good reusability and flexibility. In this paper, we present a novel formal method for program slicing, modular monadic program slicing, which abstracts the computation of program slicing as a slice monad transformer, and applies it to semantic descriptions of the program analyzed in a modular way, forming the corresponding monadic slicing algorithms. The modular abstraction mechanism allows our slicing method to possess excellent modularity and language-flexibility properties. We also give the related axioms of our slice monad transformer, the proof of the correctness and the implementation of monadic slicing algorithms. We reveal the relations of our algorithms and graph-reachable slicing algorithms.展开更多
基金Supported by the Natural Science Research Plan for High School of Jiangsu Province (Grant No. 05KJD520151)
文摘Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular computation. The current slicing methods, however, are singular （mainly based on a program or system dependence graph）, and lack good reusability and flexibility. In this paper, we present a novel formal method for program slicing, modular monadic program slicing, which abstracts the computation of program slicing as a slice monad transformer, and applies it to semantic descriptions of the program analyzed in a modular way, forming the corresponding monadic slicing algorithms. The modular abstraction mechanism allows our slicing method to possess excellent modularity and language-flexibility properties. We also give the related axioms of our slice monad transformer, the proof of the correctness and the implementation of monadic slicing algorithms. We reveal the relations of our algorithms and graph-reachable slicing algorithms.
