Question

This subsection defines inductively how local variable names flow through unclocked sequences. Below, “U”

denotes set union, “ ” denotes set intersection, “–” denotes set difference, and “{}” denotes the empty set.

The function “sample” takes a sequence as input and returns a set of local variable names as output. Intuitively,

this function returns the set of local variable names that are sampled (i.e., assigned) in the sequence.

The function “block” takes a sequence as input and returns a set of local variable names as output. Intuitively,

this function returns the set of local variable names that are blocked from flowing out of the sequence.

The function “flow” takes a set X of local variable names and a sequence as input and returns a set of local variable

names as output. Intuitively, this function returns the set of local variable names that flow out of the

sequence given the set X of local variable names that flow into the sequence.

The function “sample” is defined by

? sample (b) = {} .

? sample (( 1, v = e )) = {v} .

? sample (( R )) = sample (R) .

? sample (( R1 ##1 R2 )) = sample (R1) U sample (R2) .

? sample (( R1 ##0 R2 )) = sample (R1) U sample (R2) .

? sample (( R1 or R2 )) = sample (R1) U sample (R2) .

? sample (( R1 intersect R2 )) = sample (R1) U sample (R2) .

? sample (first_match ( R )) = sample (R) .

? sample (R [*0]) = {} .

? sample (R [*1:$]) = sample (R) .

The function “block” is defined by

? block (b) = {} .

? block (( 1, v = e )) = {} .

? block (( R )) = block (R) .

? block (( R1 ##1 R2 )) = (block (R1) – flow ({}, R2)) U block (R2) .

? block (( R1 ##0 R2 )) = (block (R1) – flow ({}, R2)) U block (R2) .

? block (( R1 or R2 )) = block (R1) U block (R2) .

? block (( R1 intersect R2 )) = block (R1) U block (R2) U ( sample (R1) sample (R2)) .

? block (first_match ( R )) = block (R) .

? block (R [*0]) = {} .

? block (R [*1:$]) = block (R) .

The function “flow” is defined by

? flow (X, b) = X .

? flow (X, ( 1, v = e )) = X U {v} .

? flow (X, ( R )) = flow (X, R) .

? flow (X, ( R1 ##1 R2 )) = flow ( flow (X, R1), R2) .

? flow (X, ( R1 ##0 R2 )) = flow ( flow (X, R1), R2) .

? flow (X, ( R1 or R2 )) = flow (X, R1) flow (X, R2) .

? flow (X, ( R1 intersect R2 )) = ( flow (X, R1) U flow (X, R2)) – block (( R1 intersect R2 )) .

? flow (X, first_match(R)) = flow (X, R) .

? flow (X, R [*0]) = X .

? flow (X, R [*1:$]) = flow (X, R) .

Remark: It can be proved that flow (X, R) = (X U flow ({}, R)) – block (R) . It follows that flow ({}, R) and block

(R) are disjoint. It can also be proved that flow ({}, R) is a subset of sample (R).