The formal semantics of program slicing for nonterminating computations. Issue 1 (4th October 2016)

• Record Type: Journal Article
• Authors: Ward, Martin; Zedan, Hussein
• Is Part Of: Journal of software. Volume 29:Issue 1(2017)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2016-10-04
• Subjects: denotational semantics -- nondeterminism -- nontermination -- program analysis -- program slicing -- wide spectrum language; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.1803
• Languages: English
• ISSNs: 2047-7473

Abstract

Abstract: 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.