A Formal Method for Program Slicing*

Yingzhou Zhang1,2, Baowen Xu1,2, Jose Emilio Labra Gayo3

1
( Dep. of Computer Science and Engineering, Southeast Univ., Nanjing 210096, China)
(2Jiangsu Institute of Software Quality, Nanjing 210096, China)
3
( Dep.of Computer Science, Univ. of Oviedo, C/Calvo Sotelo s/n C.P. 33007, Oviedo, Spain)
mathzyz@163.com, bwxu@seu.edu.cn, labra@lsi.uniovi.es

Abstract In software maintenance, program slicing can help

maintainers to determine whether a change at some
Program slicing is a well-known program analysis place in a program will affect the behavior of other
technique that extracts the elements of a program related to parts of the program. Program slicing can be used in
a particular computation. Based on modular monadic software quality assurance to locate all code that
semantics of a programming language, this paper contributes to the value of variables that might be part
presents a new formal method for slicing, called modular of a safety critical component.
monadic slicing, by abstracting the computation of The original program slicing method was expressed
slicing as a slice monad transformer. With the use of slice as a sequence of data flow analysis problems [5]. An
transformer, the feature of program slicing can be alternative approach relied on program dependence
combined in a modular way into semantic descriptions of graphs (PDG) [6]. Most of the existing slicing methods
the program analyzed. According to these, this paper were evolved from these two approaches. As the
gives both monadic dynamic and static slicing algorithms. behavior of a program is determined by the semantics of
They compute program slices directly on abstract syntax, the language, it is reasonable to expect an approach for
without the needs to explicitly construct intermediate program slicing based on formal semantics of a program.
structures such as dependence graphs, or to record an The program slicing methods focused on the
execution history in dynamic slicing algorithm. semantics of programs are mainly based on the
standard denotational semantics, i.e. denotational
slicing [7-9]. Denotational semantics, however, lack
modularity and reusability [10-14]. A practicable
1. Introduction
solution was to use monads [15] to structure
denotational semantics, with the help of monad
Program slicing is a well-known program analysis
transformers [10, 16, 17] which can transform a given
technique that extracts the elements of a program related
monad into a new one with new operations. S.Liang et
to a particular computation. A program slice consists of
al. used monads and monad transformers to specify the
those statements of a program that may directly or
semantics of programming language and called it
indirectly affect the variables computed at a given
modular monadic semantics [18]. Based on this, this
program point, referred to as a slicing criterion. Program
paper proposes a first approach for program slicing
slicing has applications in program comprehension,
based on modular monadic semantics, called modular
testing and debugging, re-engineering, and software
monadic slicing. It can compute slices directly on
maintenance [1-4].
abstract syntax, without explicit construction of
In reverse engineering, program slicing provides a
intermediate structures such as dependence graphs in the
toolset for abstracting out of the source codes the
corresponding slicers.
design decisions and rationale from the initial
The rest of the paper is organized as follows: In
development and understanding the algorithms chosen.
Section 2, we briefly introduce the fundamental concepts
of modular monadic semantics through a simple
* example language. The monadic program slicing
This work was supported in part by the National Natural Science
algorithms and their complexity are discussed in Section
Foundation of China (60373066, 90412003), Young Scientist's
3. In Section 4, we illustrate our monadic slicing
Foundation of NSFC (60303024), National Research Foundation for
algorithm by analyzing in detail a sample of the example
the Doctoral Program of Higher Education of China (20020286004).
language, with the results from our slicer prototype tool typical denotational semantic description.
under development. In Section 5, our novel algorithms Moggi realized that for realistic semantics features
are discussed in associated with related works. We had to be combined, and so he presented monad
conclude this paper with directions for future work in constructors that could add new notions of
Section 6. computation to a monad. D.Espinosa called them
monad transformers in his system Semantic Lego [17].
2. Preliminaries A monad transformer consists of a type constructor t
and an associated function liftt, where t maps any given
Monads were discovered in category theory in the monad (m, returnm, bindm) to a new monad (t m,
1950s and introduced to the semantics community by returnt m, bindt m); liftt is a function of type:
Moggi in [15]. Monads are an abstract technique for liftt : m a → t m a
encapsulating details of impure features such as states, Monad transformers provide the power needed to
nondeterminism and I/O used by the computations. represent the abstract notion of programming language
Formally, a monad is a triple (m, returnm, bindm), features, but still allow us to access low-level semantic
where m is a type constructor (a map from each type a details. Multiple monad transformers can be composed
to a corresponding type m a); returnm and bindm are to form the underlying monad used for the semantic
two primitive operators: specification of the high-level language.
returnm :: a → m a
bindm :: m a → (a → m b) → m b S :: = ide := l.e | S1; S2 | skip
returnm a is a trivial computation that just return a as | read ide | write l.e
the result, whereas m ‘bindm’ k computes m and passes
| if l.e then S1 else S2 endif
the result to the rest of the computation k.
Intuitively, a monad is a transformation on types | while l.e do S endwhile
equipped with a composition method for transformed Figure 2. Abstract syntax of W
values. To add a new feature to a monadic semantics,
we only need to add a semantic description of the new
feature, and change the underlying monad, but not the The key of modular monadic semantics is the
semantic descriptions of the existing features. division of the monad m into a series of monad
Traditional denotational semantics maps, say, a term, transformers, each representing a computation. What’s
an environment and a continuation to an answer. In more, monad transformers can be designed once and
contrast, monadic semantics maps terms to for all [12], because they are entirely independent of
computations, where the details of the environment, the language being described. Inspired by this, we try
store, etc. are “hidden”. The monadic style in which to abstract the computation of program slicing as a
the descriptions are written is far easier to read than a monad transformer. This will be discussed in next
section.

Environment monad transformer: State monad transformer:

type EnvT ρ m a = ρ → m a type StateT s m a = s → m (s, a)
returnEnvT ρ m x = λρ. returnm x returnStateT s m x = λs. returnm (s, x)
x ‘bindEnvT ρ m’ f = λρ. {a ← x ρ ; f a ρ}m x ‘bindStateT s m’ f = λs. {(s′, a) ← x s ; f a s′}m
liftEnvT ρ x = λρ. x ‘bind m’ returnm = λs. {a ← x ; returnm (s, a)}m
= λρ. returnm ρ = λs. returnm (s, s)
liftStateT s x

inEnv ρ x = λ_. x ρ = λ_. returnm ((), s)

rdEnv getState
setState s

Error monad transformer: Input-Output monad transformer:

type Err a = Ok a | Err String type IOT m a = String → m (a, String)
type ErrT m a = m (Err a) returnIOT m a = λs. returnm (a, s)
returnErrT m x = returnm (Ok x) x ‘bindIOT m’ f = λs. {(a, s′) ← x s ; f a s′}m
x ‘bindErrT m’ f = { a ← x ; case a of = λs. {a ← x; returnm (a, s)}m
= λs. returnm (s, s)
liftIOT s x
Ok y : f y
putvalue s = λ_. returnm (s, ())
getvalue
Err s: returnm (Err s) }m
liftErrT x = {a ← x; returnm (Ok a) }m
err s = returnm (Err s)

Figure 1. Some common monad transformers

 Figure 1 describes some common monad transformers denotes a fixpoint operator; xtdEnv and lkpEnv are the
which are similar to the ones given in [12, 15, 16, 18, 19]. update and lookup operator of environments Env,
For the purpose of this paper, we will focus our respectively; updSto is the update function of stores
attention on a simple imperative language W. Its abstract Loc; rdEnv and inEnv, putValue and getValue are the
syntax is provided in Figure 2, where S ranges over basic operators of EnvT and IOT showed in Figure 1,
statements Stmt, ide ranges over a set of identifiers respectively.
Ide, and l.e range over a set of labeled expressions To conveniently discuss program slices later,
Exp. The expressions, whose syntax is left unspecified following G.A.Venkatesh’s idea in [9], we define
for the sake of generality, are uniquely labeled. We Syn(s, L) for language W in Figure 4, where s is a W-

criterion, ε null result, and Refs(l.e) the set of variables

assume that the labeled expressions have no side-effects. program analyzed, v the variable of interest in a slicing
In modular monadic semantics, the monad definition is
simply a composition of the corresponding monad occurring in expression l.e. It guides us how to
transformers, applied to a base monad. In this paper, construct a syntactically valid subprogram of s from
we use the input/output monad IO as the base monad. the set of labels of labeled expressions L. Furthermore,
We then select some monad transformers such as EnvT, it allows us to concentrate on the labeled expressions
StateT, ErrT showed in Figure 1, and apply them to the in a program analyzed, since they are predominant
base monad IO, forming the resulting monad ComptM: parts in a program slice, and other parts can be
ComptM ≡ (EnvT ⋅ StateT ⋅ ErrT) IO
captured through Syn(s, L).

Now the formal semantic description of language W

can be given in Figure 3. In Figure 3, the identifier Fix

Domains:
loc: Loc (Stores); v: Value (Values)
Semantics Functions:
S :: Stmt → ComptM ()
E :: Exp → ComptM Value
S ide := l.e = {v ← E l.e ; loc ← lkpEnv(ide, rdEnv); updSto(loc, return v)}
S S1; S2 = {S S 1 ; S S2 }
skip = return ()
if l.e then S 1 else S 2 endif = {v ← E l.e ;
S

case v of tt → S S 1 ;
S

ff → S S 2 }
S while l.e do S endwhile = Fix (λf.{v ← E l.e ;
case v of tt → f ⋅ S S ;
ff → return () } )
S read ide = {loc ← lkpEnv(ide, rdEnv); v ← getValue; updSto(loc, return v)}
S write l.e = { v ← E l.e ; putValue (return v) }

Figure 3. Modular monadic semantics of W

Syn(s, L) =

if l ∈ L then “ide := l.e” else ε

case s of
“ide := l.e ” :

ε
“S1; S2 ” : Syn(S1, L); Syn(S2, L)

if ide ∈ {v} ∪ U Re fs ( l.e ) then “read ide” else ε

“skip ” :
“read ide ” :
l∈ L

if v ∈ Refs(l.e) then “write l.e” else ε

“if l.e then S1 else S2 endif ” : if (Syn(S1, L) = Syn(S2, L) = ε)∧(l ∉ L) then ε
“write l.e ” :

“while l.e do S endwhile ” : if (Syn(S, L) = ε)∧(l ∉ L) then ε

else “if l.e then Syn(S1, L) else Syn(S2, L) endif ”

else “while l.e do Syn(S, L) endwhile ”

Figure 4. The definition of Syn(s, L)

3. Modular Monadic Program Slicing Based on modular monadic semantics of a program
language, the monadic algorithms for dynamic slicing
3.1 Slice Monad Transformer and static slicing are provided in Figure 6 (where
INPUT denotes the actual input during an execution),
In this section, we try to abstract the computation of and Figure 7 respectively. These two algorithms are
program slicing as an independent entity, slice monad very similar except for Step 3. The main idea of monadic
transformer. This work is significant because a monad slicing algorithm can be briefly stated as follows: for
transformer can be designed once and for all. We give obtaining the program slice w.r.t. a slicing criterion, we
the definition of slice monad transformer in Figure 5, firstly apply the program-slice transformer SliceT to
where L denotes a set of labels of expressions that semantic description of the program analyzed. It makes
were required to compute the current expression. the resulting semantic description include the program-
A slice monad transformer SliceT L m, takes an slice semantic feature. According to this semantic
initial set of labels, and returns a computation of a pair description, we then execute this program with an
of the resulting value and the new set of labels. The input (for dynamic slicing) or analyze each statement
lifting function liftSliceT L says that a computation in the in sequence (for static slicing). Finally we will obtain
monad m behaves identically in the monad SliceT L m the program slices of all single variables in the
and makes no changes to the set of labels. The operation program, including the program slice of the variable of
updateSlice supports update of program slices. interest.
In form, the slice monad transformer is similar to the In Step 1, we initialize the set of labels, L, and all
state monad transformer. So, the correctness proof of original slices in the table Slices with null set. The data
its definition can be obtained easily by following the structure of program slices Slices is defined as follows:
proofs for transformer StateT in [12] or [20]. type Var = String
type Labels = [Int]
Slice monad transformer:
type SliceT L m a = L → m (a, L)
type Slices = [(Var, Labels)]

returnSliceT L m x = λL. returnm (x, L)

getSli :: ComptM Slices
setSli :: Slices → ComptM Slices
m ‘bindSliceT L m’ f = λL. {(a, L′) ← m L; f a L′}m lkpSli :: Var → Slices → ComptM Labels
liftSliceT L m = λL. {a←m; returnm (a, L)}m xtdSli ::
updateSlice f = λL. returnm (f L, L) (Var, ComptM Labels)→Slices→ComptM ()
mrgSli :: Slices → Slices → ComptM Slices
Figure 5. Slice monad transformer where [] denotes a table data structure. Five operators
getSli, setSli, lkpSli, xtdSli and mrgSli, represent to
3.2 Monadic Program Slicing Algorithms return and setup the current table of program slices,
lookup, update and merge a slice corresponding to a
For simplicity, we only consider end slicing with variable in a given table of slices, respectively.
respect to a slicing criterion <p, v>, where p is the end In Step 2, we want to combine the feature of
point of a program, and v a variable. This can be easily program slicing into semantic descriptions through
generalized to a set of points and a set of variables at each monad transformer SliceT given in Figure 5. As for
point by taking the union of the individual slices [2]. language W, we compose SliceT with other transformers

Input: Slicing criterion <INPUT, p, v> Input: Slicing criterion <p, v>
Output: Dynamic slice Output: Static slice
1. Initialize the set L and the table Slices. 1. Initialize the set L and the table Slices.
2. Add the feature of program slicing into 2. Add the feature of program slicing into
semantic descriptions in a modular way, semantic descriptions in a modular way,
through slice transformer SliceT. through slice transformer SliceT.
3. Execute the program analyzed with INPUT in 3. Compute static slices of each statement in
accordance with the semantic description in sequence basing on the semantic description in
Step 2, obtaining the final Slices. Step 2, obtaining the final Slices.
4. Returning the final dynamic slicing result 4. Returning the final static slicing result
according to Slices and Syn(s, L), where L = according to Slices and Syn(s, L), where L =
lkpSli (v, getSli). lkpSli (v, getSli).
Figure 6. Dynamic slicing algorithm Figure 7. Static slicing algorithm
(e.g. EnvT, StateT, ErrT) to form the resulting monad L′ ← {l} ∪ L ∪ U lkpSli ( r , getSli ) ;
ComptM as follows: r ∈ Re fs ( l.e )

ComptM ≡ (SliceT ⋅ StateT ⋅ EnvT ⋅ ErrT) IO T ← getSli;

T′ ← {f L′⋅ S L′; getSli};
where the order of monad transformers can be changed
mrgSli(T, T′) } )
at random. Meanwhile, we need to reify the intermediate
set L′ in bindSliceT L m as following: The correctness proofs of our program slicing
L′ = {l} ∪ L ∪
algorithm can refer to the way in [9, 22]. Informally,
U lkpSli ( r , getSli ) (*) the term L and
r ∈ Re fs ( l.e )
U lkpSli ( r , getSli ) in the definition
r ∈ Re fs ( l.e )
This relation reflects when and how to change the set L. of L′ (see Equation (*)) can capture control
In addition, for recording the result of program slicing, dependences between statements and data dependences
we ought to add the operator xtdSli into semantic between variables, respectively.
descriptions of assignment statements as the following
bold terms: 3.3 The Complexity of the Algorithms
ide := l.e
= λL.{ v ← E l.e ; In this section, we will analyze the complexity of
L′ ← {l} ∪ L ∪ U lkpSli ( r , getSli ) ; the monadic slicing algorithms presented in Section
r ∈ Re fs ( l.e ) 3.2. The measures of system size used below are those
loc ← lkpEnv(ide, rdEnv); associated with the data structure of program slice
updSto(loc, return v); Slices (which is a Hash table).
xtdSli(ide, L′, getSli) } In a monadic compiler/interpreter, our slice monad
transformer could be modularly and safely combined
Similar to the way in forward dynamic slicing [21],
into the semantic buildings, so the complexity analysis
in our modular monadic approach, the program slices
for associated variables of each statement are computed is restricted to L′ and Syn(s, L) of a concrete
immediately after this statement is executed/analyzed. programming language. The intermediate label set L′
After the last statement is executed/analyzed, the can be determined in time O(v), where v refers to the
individual program slices for all variables of the number of single variables in the program
program executed have been obtained. analyzed/executed. To determine the Syn(s, L) shown
Concretely, in monadic dynamic slicing algorithm, in Figure 4 may cost O(m), where m is the number of
we compute dynamic slices while executing the labeled expressions in the program. Therefore the time
cost of the predominant part of program slicing in the
monadic slicing algorithm is bounded by O(v × n),
program analyzed with INPUT (cf. Step 3 in Figure 6),
according to the semantic description including the
feature of program slicing. After the last statement is where n is the number of all labeled expressions
executed, we obtain a table Slices that includes appeared (perhaps repeatly) in the sequence of
analyzing/executing the program. In addition, an extra
time cost O(v × m) needs to get the executable slices of
individual dynamic slices for all variables. In contrast,
in static slicing algorithm, we need to capture the
all single variables. Now we can see that the total time
cost is O(v × n + v × m). Since we finally obtain the
statements that possibly affect the variable in the
slicing criterion, besides those that actually affect this
variable as dynamic slicing do. Therefore, we ought to slices of all variables after the last statement is
analyzed/executed, the program slice of each variable,
on the average, costs O(n +m), which is linear.
modify semantic descriptions of conditional statement
and loop statement, and to add in the operator mrgSli
as following. To analyze the space complexity of the algorithms,
we pay our attention to the constructions Refs(l.e),
Slices, L′ and L. We need space O(v × v) and O(v × m)
if l.e then S1 else S2 endif
= λL.{ v ← E l.e ;
L′ ← {l} ∪ L ∪ U lkpSli ( r , getSli ) ;
to save Refs(l.e) and Slices, respectively. According to
r ∈ Re fs ( l.e )
the definition of slice monad transformer SliceT in
T ← getSli ;T1 ← { S1 L′; getSli};
Figure 1, we need to introduce more intermediate
setSli(T); T2 ← { S2 L′; getSli};
labels when SliceT is applied to loop statements (eg.
while statements), and can allocate a same space to the
mrgSli(T1, T2) }
intermediate labels L′ of other statements. So it takes
while l.e do S endwhile the space O(k × m) to save intermediate labels, where k
= Fix (λf. λL.{v ← E l.e ; refers to the maximal times of analyzing/executing the
loop statements in the program. The label set L will O(v × v + v × m + k × m), which is irrelated to n.
cost the space O(m). Therefore, the total space cost is

(1) Source program (2) Dynamic slice w.r.t s

1 read n ; 1 read n ;
2 read a ; 2 read a ;
3 i := 1 ; 3 i := 1 ;
4 s := 1 ; 4 s := 1 ;
5 if (a > 0) then
6 s := 0
else skip endif ;
7 while (i <= n) do 7 while (i <= n) do
8 if (a > 0) then 8 if (a > 0) then
9 s := s + 2
10 else s := s * 2 endif 10 else s := s * 2 endif
11 i := (i + 1) ; 11 i := (i + 1) ;
endwhile ; endwhile ;
12 write (s + 4) 12 write (s + 4)

Figure 8. A sample W-program and its slice w.r.t <(a=0, n=2), 20, s>

4. A Case Study Lastly, as stated in monadic dynamic slice algorithm,

the dynamic slices for associated variables of each
This section illustrates the dynamic slicing algorithm instruction are computed immediately after this
proposed in Figure 6 through the example W-program instruction is executed. In detail, while instructions in
given in Figure 8 (1). We will use our modular the above sequence list are being executed, the initial
monadic algorithm to compute the dynamic slice with set L and dynamic slice table Slices are modified,
respect to <(a=0, n=2), 12, s>. according to Step 2 and 3 in our algorithm. In other
We firstly label each expression in the example words, after a labeled expression is executed, the set L
program with a unique label. Here we employ the line
is transformed into intermediate set L′ through
number of position where the expression occurs in
Equation (*), and this new set will be passed down the
source program. The resulting labeled expressions l.e
rest of the execution of the corresponding whole
and their corresponding set Refs(l.e) are showed in
statement to this expression. Moreover, if this
Figure 9.
statement is an assignment one, the dynamic slice
Then, let INPUT is a=0 and n=2, and execute the
Slices need to update through the term xtdSli (ide, L′,
program with INPUT according to the modular monadic
getSli).
semantics that includes the feature of program slicing.
For instance, at the beginning of executing for first
The following set is corresponding execution list,
time the 10th instruction in above list, the corresponding
which comprises labels of instructions (i.e. statements
table Slices is showed in Figure 10 (1). At one time, the
or their snippets) that are the same order as they have
initial set L, passing through executions of the 7th and
been executed:
{1, 2, 3, 4, 5, 7, 8, 10, 11, 7, 8, 10, 11, 7, 12 } 8h instruction, is turned into an intermediate set L′′ as
follows:
L′′ = {8} ∪ L′ ∪ lkpSli (a, getSli) = {3, 7, 8}
l. e Refs(l.e)
3. i := 1 {i}
4. s := 1 {s} where
L′= {7}∪L ∪ (lkpSli(i, getSli) ∪ lkpSli(n, getSli))
5. a > 0 {a}
6. s := 0 {s}
7. i <= n {i,n} = {3, 7}
8. a > 0 {a} After the first 10th instruction is executed, the
9. s :=s+2 {s} intermediate set is changed to L′′′:
L′′′ = {10} ∪ L′′ ∪ lkpSli (s, getSli)
10. s :=s*2 {s}

= {10} ∪ {3, 7, 8} ∪{4}

11. i :=i+1 {i}
12. s + 4 {s}
Figure 9. l.e and Refs(l.e) = {3, 4, 7, 8, 10}
 Furthermore, the 10th is an assignment one, so the Figure 8 (2), with respect to slice criterion <(a=0,n=2),
related data in Slices need to update through xtdSli. 12, s>.
Here L′′′ replaces the dynamic slice of variable s before On the basis of Labra’s language prototyping system
execution, and now the table Slices is given in Figure LPS [23], which facilitates the modular development
10 (2). Going on in this way until finishing the of interpreters from modular monadic semantics, we
execution of the last instruction (i.e. 12th) in above are now developing a monadic slicer [24]. As for this
sequence list, we will obtain the final Slices as shown example, we can obtain the result (shown in Figure 11)
in Figure 10 (3). According to it and Syn(s, L), we from the current monadic slicer, where we didn’t
could get the final result of dynamic slice, shown in consider the function Syn(s, L) and directly include the
Read and Write statements in the results.

(1) before execute first 10th (2) after execute first 10th (3) after execute the last instruction

Var Labels Var Labels Var Labels

n φ n φ n φ
a φ a φ a φ
i {3} i {3} i {3, 7, 11}
s {4} s {3, 4, 7, 8, 10} s {3, 4, 7, 8, 10, 11}

Figure 10. Slices during execute instructions with INPUT

READ 1 ds = [("n",[1])]
READ 2 ds = [("n",[1]),("a",[2])]
ASSIGN 3 ds' = [("n",[1]),("a",[2]),("i",[3])]
ASSIGN 4 ds' = [("n",[1]),("a",[2]),("i",[3]),("s",[4])]
IF 5 ds = [("n",[1]),("a",[2]),("i",[3]),("s",[4])]
WHILE 7 ds = [("n",[1]),("a",[2]),("i",[3]),("s",[4])]
IF 8 ds = [("n",[1]),("a",[2]),("i",[3]),("s",[4])]
ASSIGN 10 ds' = [("n",[1]),("a",[2]),("i",[3]),("s",[1,2,3,4,7,8,10])]
ASSIGN 11 ds' = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10])]
WHILE 7 ds = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10])]
IF 8 ds = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10])]
ASSIGN 10 ds' = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10,11])]
ASSIGN 11 ds' = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10,11])]
WHILE 7 ds = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10,11])]
WRITE 12 ds = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10,11,12])]
Value = Left 8
DSlices = [("n",[1]),("a",[2]),("i",[1,3,7,11]),("s",[1,2,3,4,7,8,10,11,12])]

Figure 11. The dynamic slicing result from our monadic slicer

satisfy the condition are deleted from the slice.

5. Related Work M.Harman et al.’s amorphous slicing [26] allows for
any simplifying transformations which preserve this
Most of the existing slicing algorithms rely on semantic projection. These two methods are not
relation graphs such as system dependence graphs directly based on formal semantics of a program.
(SDG) or program dependence graphs (PDG). A few P.A.Hauser’s denotational slicing [7, 8] employs the
program slicing methods focused on the semantics of functional semantics of a program language in the
programs. denotational (and static) program slicer. Venkatesh
G.Canfora et al.’s conditioned slicing [25] adds a also took account of denotational slicing with formal
condition in a slicing criterion. Statements that do not slicing algorithms including dynamic and static [9]. This
approach is indeed based on the standard denotational
semantics of a program language. Inspired by this, we In our future work, we will consider modular
have proposed a new formal method for program monadic slicing in the present of aliasing, pointer and
slicing, called modular monadic slicing, which is array. At the same time, we will complete our
based on modular monadic semantics. prototype of monadic slicer and present the
Compared with the existing slicing methods, the comparisons with other slicing methods in experiment.
modular monadic slicing has excellent flexibility and
reusability properties, because it have abstracted the
computation of program slicing as an language- Acknowledgements
independence object, slice monad transformer. The
modular monadic slicing can compute slices directly The authors thank several anonymous referees for
on abstract syntax, without explicit construction of their constructive reviews and comments.
intermediate structures such as data flow graphs or
dependence graphs in slicers. Despite this, it is still
feasible, because there is a clear operational Reference
interpretation of modular monadic semantics, and
some modular compilers/interpreters using monad [1] F. Tip, “A Survey of Program Slicing Techniques”,
transformers have already been constructed in [11, 12, Journal of Programming Languages, 1995, vol. 3, no. 3,
18, 20, 23, 27]. pp. 121-189.
In respect of efficiency, our monadic algorithms are [2] D.Binkley, and K.B. Gallagher, “Program Slicing”,
not less precise than PDG-based ones as shown from the Advances in Computers, 1996, vol. 43, pp. 1-50.
example in Section 4. This is because the term L and [3] M. Kamkar, “An Overview and Comparative Classification
of Program Slicing Techniques”, Journal of Systems and
U lkpSli ( r , getSli ) in the definition of L′ can
r ∈ Re fs ( l.e )
Software, 1995, vol. 31, no. 3, pp. 197-214.
[4] M. Harman, and R.M. Hierons, “An Overview of Program
accurately capture control dependences and data Slicing”, Software Focus, 2001, vol. 2, no. 3, pp. 85-92.
dependences respectively, which are the base of PDG- [5] M. Weiser, “Program Slicing”, IEEE Transaction on
based algorithms. According to the complexity analysis Software Engineering, 1984, vol. 16, no. 5, pp. 498-509.
in Sections 3.3, the space complexity is irrelated to the [6] K.J. Ottenstein, and L.M. Ottenstein, “The program
length of the program analyzed/executed; the time dependence graph in a software development environment”,
complexity of each variable is averagely linear, i.e. ACM SIGPLAN Notices, 1984, vol.19, no. 5, pp. 177-184.
O(n + m). [7] P.A. Hausler, “Denotational Program Slicing”, Proceeding
of 22th Annual Hawaii International Conference on System
Sciences, 1989, vol. 2, pp. 486-495.
6. Summaries [8] L. Ouarbya, S. Danicic, M. Daoudi, M. Harman, and C.
Fox, “A Denotational Interprocedural Program Slicer”,
Program slicing is an important decomposition Proceeding of 9th IEEE Working Conference on Reverse
technique. It can be roughly classified as static slicing Engineering, IEEE Press, Virginia, 2002, pp. 181-189.
and dynamic slicing, according to whether they only [9] G. A. Venkatesh, “The Semantic Approach to Program
use statically available information or compute those Slicing”, ACM SIGPLAN Conference on Programming
Language Design and Implementation, Toronto, Canada,
statements that influence the value of a variable
1991, pp. 26-28.
occurrence for a specific program input. It has been [10] E.Moggi, “Notions of Computation and Monads”,
widely used in many software activities, such as Information and Computation, 1991, vol. 93, pp. 55-92.
software analyzing, understanding, debugging, testing, [11] S. Liang, and P. Hudak, “Modular Denotational
and maintenance. Semantics for Compiler Construction”, Proceeding of 6th
In this paper, we have proposed a novel approach European Symposium on Programming Languages and
for program slicing; called it modular monadic Systems, ESOP’96. LNCS 1058, Springer-Verlag, Berlin,
program slicing as it is based on modular monadic 1996, pp. 219-234.
semantics. It has excellent flexibility and reusability [12] K. Wansbrough, “A Modular Monadic Action
Semantics”, Master thesis, University of Auckland,
properties comparing with the existing program slicing
Auckland, 1997.
algorithms. Furthermore, it is feasible, because modular [13] P.D. Mosses, “Semantics, Modularity, and Rewriting
monadic semantics is executable and some modular Logic”, Proceeding of 2nd International Workshop on
compilers/interpreters have already been existed. We Rewriting Logic and its Applications, ENTCS 15,
now developed a program-slice prototype based on a Elsevier Press, Netherlands, 1998.
modular monadic interpreter [23, 24]. [14] J. Power, “Modularity in Denotational Semantics”,
Proceeding of 13th Annual Conference on Mathematical
 Foundations of Programming Semantics, Elsevier Press, [21] G.Tibor, B. Árpád, and F. István, “An Efficient
New York, 2000. Relevant Slicing Method for Debugging”, Software
[15] E. Moggi, “An Abstract View of Programming Engineering Notes, Software Engineering-ESEC/FSE’99
Languages”, LFCS Report, ECS-LFCS-90-113, University Springer ACM SIGSFT, 1999, vol. 24, no. 6, pp. 303-321.
of Edinburgh, 1989. http://www.lfcs.informatics.ed.ac.uk [22] G. A. Venkatesh, “Semantics of program slicing”,
/reports/90/ECS-LFCS-90-113/. Bellcore TM-ARH-018561, 1990.
[16] P. Wadler, “Comprehending monads”, ACM Conference [23] J.E. Labra Gayo, M.C. Luengo Diez, J.M. Cueva
on Lisp and Functional Programming, ACM Press, Lovelle, and A. Cernuda del Rio, “A Language
France, 1990, pp. 61-78. Prototyping System Using Modular Monadic Semantics”,
[17] D. Espinosa, “Semantic Lego”, PhD dissertation, Workshop on Language Definitions, Tools and
Columbia University, Columbia, 1995. Applications, LDTA’01, Netherlands, 2001.
[18] S. Liang, P. Hudak, and M. Jones, “Monad Transformers [24] Website. https://sourceforge.net/projects/lps.
and Modular Interpreters”, 22nd ACM SIGPLAN-SIGACT [25] G. Canfora, A. Cimitile, and A. De Lucia, “Conditioned
Symposium on Principles of Programming Languages, Program Slicing”, Information and Software Technology,
POPL’95, ACM Press, New York, 1995, pp. 333-343. 1998, vol. 40, no. 11/12, pp. 595-607.
[19] J.E. Labra Gayo, M.C. Luengo Diez, J.M. Cueva [26] M. Harman, and S. Danicic, “Amorphous Program
Lovelle, and A. Cernuda del Rio, “Reusable Monadic Slicing”, IEEE International Workshop on Program
Semantics of Object Oriented Programming Languages”, Comprehension, IWPC’97, IEEE CS Press, Los Alamitos,
Proceeding of 6th Brazilian Symposium on Programming 1997, pp. 70-79.
Languages, SBLP’02, PUC-Rio University, Brazil, 2002. [27] W. Kahl, “A Modular Interpreter Built with Monad
[20] S. Liang, “Modular Monadic Semantics and Compilation”, Transformers”, Lectures on Functional Programming,
PhD dissertation, University of Yale, Yale, 1998. CAS 781, 2003. http://www.cas.mcmaster.ca/~kahl/FP/
2003/