A novel formal approach to program slicing  

作　　者：ZHANG YingZhou 

机构地区：[1]College of Computer, Nanjing University of Posts and Telecommunications, Nanjing 210003, China [2]Institute of Computer Technology, Nanjing University of Posts and Telecommunications, Nanjing 210003,China

出　　处：《Science in China(Series F)》2007年第5期657-670,共14页中国科学（F辑英文版）

基　　金：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.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.

关 键 词：program slicing MONADS MODULARITY slice monad transformer formal semantics 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]