(Last modified Thu Apr 17 22:42 2008)

Definitions

definition of variable x

A statement that assigns or may assign a value to x. 

Examples: 

• an assignment to x;
• an assignment to x through a pointer that references x;
• an assignment within another method or procedure that affects a reference to x;
• if x is an object or structure, a change to a part of x's state. 

reaches

A definition of x reaches a statement S if the value of x at S could still be the one given by that definition.

gen[S]

The set of definitions generated by statement S.  For example, an assignment generates a definition. 

kill[S]

The set of definitions killed by statement S; that is, the set of definitions that S renders ineffective.  For example, if S generated a definition of variable y, then S kills any earlier definitions of y. 

in[S]

The set of definitions reaching the beginning of S, taking the entire program and its context into account.

The in set of the first statement in a program is empty.  The in set of every other statement in a program is the union of the out sets of all statements that can immediately precede it. 

out[S]

The set of definitions reaching the end of S, taking the entire program and its context into account.

gen, kill, and out for some statements

Definition S — "d: a=expression"

1. gen[S] = {d}
2. kill[S] = {all definitions of a} - {d}
3. out[S] = gen[S] ∪ (in[S] - kill[S])

Sequence S — "Q then R"

1. gen[S] = gen[R] ∪ (gen[Q] - kill[R])
2. kill[S] = kill[R] ∪ (kill[Q] - gen[R])
3. out[S] = out[R]

• in[Q] = in[S]
• in[R] = out[Q]

Alternation S — "Q or R"

1. gen[S] = gen[Q] ∪ gen[R]
2. kill[S] = kill[Q] ∩ kill[R]
3. out[S] = out[Q] ∪ out[R]

• in[Q] = in[S]
• in[R] = in[S]

Iteration S — "Q 1 or more times"

1. gen[S] = gen[Q]
2. kill[S] = kill[Q]
3. out[S] = out[Q]

• in[Q] = in[S] ∪ gen[Q]

Dwyer and Clarke's framework

Dwyer and Clarke's framework consists of five mathematical objects:

Thomas A. Alspaugh
Assistant Professor, Informatics Dept.
School of Information and Computer Sciences