The formal semantics of program slicing for nonterminating computations

详细信息    查看全文

• 作者：Martin Ward and Hussein Zedan
• 刊名：Journal of Software: Evolution and Process
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：29
• 期：1
• 全文大小：2185K
• ISSN：2047-7481

文摘

Since the original development of program slicing in 1979 there have been many attempts to define a suitable semantics, which will precisely define the meaning of a slice. Particular issues include handling termination and nontermination, slicing nonterminating programs, and slicing nondeterministic programs. In this paper we review and critique the main attempts to construct a semantics for slicing and present a new operational semantics, which correctly handles slicing for nonterminating and nondeterministic programs. We also present a modified denotational semantics, which we prove to be equivalent to the operational semantics. This provides programmers with 2 different methods to prove the correctness of a slice or a slicing algorithm and means that the program transformation theory and FermaT transformation system, developed last 25 years of research, and which has proved so successful in analyzing terminating programs, can now be applied to nonterminating interactive programs.