4.2. Static Slice of First-Order Functional Languages

We have classified subexpressions according to the informal usage relation to the accumulation parameter and results of recursions. In this section, we define static slicing of our language to define usage relations between subexpressions.

A program slice consists of the parts of a program that affect the values computed at some designated program point referred to as a slicing criterion[23]. Static slicing isolates parts of a program that potentially affect the values computed at slicing criterion over all possible inputs. Program slicing can be used for debugging, program optimization such as dead code elimination and parallelization of sequential programs.

Figure 2: Denotational Semantics of Input Language

We define a static slice using the denotational collecting semantics of our language. Our semantics returns not only the resulting value of the expression but also a collection which stores all the evaluated values for each subexpression during the program execution. The semantics shown in Figure 2 is composed of the semantic functions $E_M$ for expressions, $U_M$ for function definitions and the pattern matching rules. The subscription $M$ is a set of labels, which represents the set of subexpressions whose values are masked. By replacing values evaluated from masked subexpressions with $!$, we can isolate subexpressions which use values of masked subexpressions or variable patterns.

Figure 3: Sets and Domains

Figure 4: Auxiliary Functions used in the Semantics

Sets and domains used in the semantics are shown in Figure 3. $Val_\bot$ means a flat cpo with the least element $\bot$. $Collection$ is a function domain which maps a label to a set of values evaluated from the subexpression designated with the label. $Fval$ is a domain for semantic values of functions. A function value maps a value to a tuple of an output value and a collection.

Auxiliary functions used in the semantics are shown in Figure 4. The $Eval$ function returns $!$, if the input value has $!$ as its part. This function is used in the semantic rules for primitive operations and pattern matching of variable patterns. In primitive operations, if any operand value has $!$ as its part, the result becomes $!$. In pattern matching, if a value matched to a variable pattern has $!$ as its part, the variable is mapped to $!$ in the resulting environment. The $\bigcup$ operator is used to sum collections. Resulting collection from the $\bigcup$ operator returns the sum of the results of summed collections for a given label. So, in the semantic rules the resulting collection maps a label to a set of all the values which have been computed from the designated expression. The $\oplus$ operator is used to sum environments. It overwrites the return values of the left environment with the return values of the right environment.

The semantic functions shown in Figure 2 have following types :

$$\begin{array}{lll} U_M~:~\mathit{Fdef} \rightarrow Fval \\ ... ...al}_\bot) \rightarrow (Env \times Collection) \\ \end{array}$$

$U_M$ rule returns a function value given a function definition using the fixed point semantics of recursions. $E_M$ evaluates an expression under an environment for variables and function names. It returns a value and a collection. The resulting collection stores all the values that have been evaluated from each subexpression. Given a pattern and a value, $\models_M$ rule returns a variable environment and a collection which stores all the matched values for each pattern variable.

Each rule of $E_M$ is composed of two alternatives for each case. With the second alternatives only, the semantic rules are the same as a usual denotational semantics. Each rule evaluates the value of an expression under a given environment and returns an evaluated value and a collection. The first alternatives are added to express the effect of values from subexpressions whose labels are in $M$. When the label of an evaluated expression is in $M$, the resulting value is not used as an output value and $!$ is returned instead. So, expressions which use the value of masked expressions use $!$ for their evaluation. Because any evaluation which uses the value $!$ always results in a value having $!$ as its part, we can identify the effect of the masked expressions on any expression.

Now we can formally define a static slice as follows.

Definition 2   Static Slice
Given a function definition ${\mathit fdef} = (f~p_1 = e_1~\vert \ldots \vert~p_n = e_n)$, and a slicing criterion $l \in L_f$, static slice $SS_f(l)$ is defined as follows, where $L_f$ is the set of labels in $e_1,\ldots,e_n$.

$$\begin{array}{lllll} {\mathit SS}_f(l) = \{ l^\prime \in L_f... ...x{and} \\ & \exists x\in F(l)~s.t.~Eval(x) =~!~\} \end{array}$$

Given some dynamic input value which does not have $\bot$ as its part, if some value evaluated from an expression $l$ has $\bot$ as its part, it means that expression $l$ uses some value evaluated from the masked expression $l^\prime$. So $l^\prime$ is included in the static slice for $l$.

Static slices are defined based on the behaviors of a program over all possible inputs. We can analyze static slice using abstract interpretation[4,15]. The method for static slicing is not presented in this paper.

Now we can formally define the usage relation using static slicing. For two labels $l$ and $l^\prime$, $l$ uses $l^\prime$ if and only if $l^\prime \in SS(l)$.