Slicing as a program transformation

TLDR

A mathematical approach to program slicing is not tied to a particular representation and provides a sound basis for any representation. The aim of this article is to provide a unified mathematical framework for program slicing that places all slicing work for sequential programs on a sound theoretical foundation. Using WSL transformation theory, the authors define a semirefinement relation and combine it with a syntactic reduction relation and the remove statement to mathematically define backward, conditioned, static, dynamic, semantic, and operational slicing, and implement these transformations in the FermaT system. The theory also enables the concept of slicing to be applied to nondeterministic programs.

Abstract

The aim of this article is to provide a unified mathematical framework for program slicing which places all slicing work for sequential programs on a sound theoretical foundation. The main advantage to a mathematical approach is that it is not tied to a particular representation. In fact the mathematics provides a sound basis for any particular representation. We use the WSL (wide-spectrum language) program transformation theory as our framework. Within this framework we define a new semantic relation, semirefinement , which lies between semantic equivalence and semantic refinement. Combining this semantic relation, a syntactic relation (called reduction ), and WSL's remove statement, we can give mathematical definitions for backwards slicing, conditioned slicing, static and dynamic slicing, and semantic slicing as program transformations in the WSL transformation theory. A novel technique of “encoding” operational semantics within a denotational semantics allows the framework to handle “operational slicing”. The theory also enables the concept of slicing to be applied to nondeterministic programs. These transformations are implemented in the industry-strength FermaT transformation system.