title:
Formalizing Slicing


abstract:

Based on ``common knowledge'', people often expect that a static slice 
is a valid dynamic slice as well, even if overly large. However, 
there are counter examples which show that it's not always true. The
reason for this is in the definitions of the slicing techniques 
(Weiser's static slicing does not care about the path of execution,
while the dynamic slicing as defined by Korel and Laski does). The
problem is that our ``common knowledge'' does not fit to the original
definitions. However, if we have no formal background how can we 
compare existing slicing techniques, or how can we reason about them?

We have chosen the program projection theory, which is based on 
syntactic orderings and semantic equivalence relations on programs, as
the basis of our work. This work aim to build up a unified formal 
theory of slicing, where different slicing techniques can be 
compared. So far, we have been able to formalize the two most 
important slicing techniques, i.e., the static and the KL-dynamic 
one, and some new ones as a ``side effect''. With the help of this 
formalization, we have been able to compare these techniques in the
subsumes relation (which describes whether slices of one type are
always valid slices of another type of slicing) and we have been able
to rank the techniques, based on the size of minimal slices they make
possible.