Premium
The formal semantics of program slicing for nonterminating computations
Author(s) -
Ward Martin,
Zedan Hussein
Publication year - 2017
Publication title -
journal of software: evolution and process
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.371
H-Index - 29
eISSN - 2047-7481
pISSN - 2047-7473
DOI - 10.1002/smr.1803
Subject(s) - program slicing , slicing , computer science , nondeterministic algorithm , programming language , operational semantics , semantics (computer science) , denotational semantics , correctness , program transformation , transformation (genetics) , formal semantics (linguistics) , theoretical computer science , well founded semantics , biochemistry , chemistry , world wide web , gene
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.