1
$\begingroup$

I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.3 Data Flow Analysis says the following:

The least solution. The above system of equations defines the twelve sets $$\text{RD}_\text{entry}(1), \dots, \text{RD}_{\text{exit}}(6)$$ in terms of each other. Writing $\overrightarrow{RD}$ for this twelve-tuple of sets we can regard the equation system as defining a function $F$ and demanding that: $$\overrightarrow{RD} = F(\overrightarrow{RD})$$ To be more specific we can write $$F(\overrightarrow{RD}) (F_\text{entry}(1)(\overrightarrow{RD}), F_\text{exit}(1)(\overrightarrow{RD}), \dots, F_\text{entry}(6)(\overrightarrow{RD}), F_\text{exit}(6)(\overrightarrow{RD}))$$ where e.g.: $$F_\text{entry}(3)(\dots, \overrightarrow{RD}_\text{exit}(2), \dots, \overrightarrow{RD}_\text{exit}(5), \dots) = \overrightarrow{RD}_\text{exit}(2) \cup \overrightarrow{RD}_\text{exit}(5)$$ It should be clear that $F$ operates over twelve-tuples of sets of pairs of variables and labels; this can be written as $F : (\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12} \to (\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ where it might be natural to take $\mathbf{\text{Var}_\star} = \mathbf{\text{Var}}$ and $\mathbf{\text{Lab}_\star} = \mathbf{\text{Lab}}$. However, it will simplify the presentation in this chapter to let $\mathbf{\text{Var}_\star}$ be a finite subset of $\mathbf{\text{Var}}$ that contains the variables occurring in the program $\mathbf{S_\star}$ of interest and similarly for $\mathbf{\text{Lab}_\star}$. So for the example program we might have $\mathbf{\text{Var}_\star} = \{ x, y, z \}$ and $\mathbf{\text{Lab}_\star} = \{ 1, \dots, 6, ? \}$.

It is immediate that $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ can be partially ordered by setting $$\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime \ \ \ \text{iff} \ \ \ \forall i : \text{RD}_i \subseteq \text{RD}_i^\prime$$ where $\overrightarrow{\text{RD}} = (\text{RD}_1, \dots, \text{RD}_{12})$ and similarly $\overrightarrow{\text{RD}}^\prime = (\text{RD}_1^\prime, \dots, \text{RD}_{12}^\prime)$. This turns $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ into a complete lattice (see Appendix A) with least element $$\overrightarrow{\emptyset} = (\emptyset, \dots, \emptyset)$$ and binary least upper bounds given by: $$\overrightarrow{\text{RD}} \sqcup \overrightarrow{\text{RD}}^\prime = (\text{RD}_1 \cup \text{RD}_1^\prime, \dots, \text{RD}_{12} \cup \text{RD}_{12}^\prime)$$

It is easy to show that $F$ is in fact a monotone function (see Appendix A) meaning that: $$\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime \ \ \ \text{implies} \ \ \ F(\overrightarrow{\text{RD}}) \sqsubseteq F(\overrightarrow{\text{RD}})^\prime$$ This involves calculations like $$\text{RD}_\text{exit}(2) \subseteq \text{RD}_\text{exit}^\prime(2) \ \ \text{and} \ \ \text{RD}_\text{exit}(5) \subseteq \text{RD}_\text{exit}^\prime(5)$$ imply $$\text{RD}_\text{exit}(2) \cup \text{RD}_\text{exit}(5) \subseteq \text{RD}^\prime_\text{exit}(2) \cup \text{RD}_\text{exit}^\prime(5)$$ and the details are left to the reader.

Appendix A gives the following definition for monotone function:

The function $f$ is monotone (or isotone or order-preserving) if $$\forall l, l^\prime \in L_1 : l \sqsubseteq_1 l^\prime \Rightarrow f(l) \sqsubseteq_2 f(l^\prime)$$

From earlier in the textbook:

enter image description here

enter image description here

I am trying to do as the author said, and show that $F$ is a monotone function. However, I have so far been unable to make progress. It seems to me that such a proof should proceed by showing that, for some arbitrary element of the set of elements $F(\overrightarrow{\text{RD}})$, if we use the fact that $\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime$, then we can deduce that said arbitrary element is also an element of the set $F(\overrightarrow{\text{RD}})^\prime$, and so $F(\overrightarrow{\text{RD}}) \sqsubseteq F(\overrightarrow{\text{RD}})^\prime$. However, it seems to me that the textbook is very poorly written, and so it is difficult for me to even understand what said arbitrary elements of the set $F(\overrightarrow{\text{RD}})^\prime$ even are (they seem to be some kind of cartesian product, but I get very confused when trying to figure out precisely what they are). So how is it shown that $F$ is a monotone function?

$\endgroup$
0
$\begingroup$

Let me start by giving a formula for the function $F$: \begin{align*} \newcommand{\ent}{\mathsf{RD}_{\mathit{entry}}} \newcommand{\ext}{\mathsf{RD}_{\mathit{exit}}} \newcommand{\Lab}{\mathbf{Lab}} \newcommand{\bx}{\mathbf{x}} \newcommand{\by}{\mathbf{y}} \newcommand{\bz}{\mathbf{z}} &F(\ent(1),\ldots,\ent(6),\ext(1),\ldots,\ext(6)) = \\ (&\{(\bx,?),(\by,?),(\bz,?)\}, \ext(1), \ext(2) \cup \ext(5), \ext(3), \ext(4), \ext(3), \\ &(\ent(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\}, \\ &(\ent(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\}, \\ &\ent(3), \\ &(\ent(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\}, \\ &(\ent(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\}, \\ &(\ent(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\}). \end{align*} In order to show that $F$ is monotone, you need to show that the following hold whenever $\ent(i) \subseteq \ent'(i)$ and $\ext(i) \subseteq \ext'(i)$ for $i \in \{1,\ldots,6\}$:

  • $\{(\bx,?),(\by,?),(\bz,?)\} \subseteq \{(\bx,?),(\by,?),(\bz,?)\}$.
  • $\ext(1) \subseteq \ext'(1)$
  • $\ext(2) \cup \ext(5) \subseteq \ext'(2) \cup \ext'(5)$
  • $\ext(3) \subseteq \ext'(3)$
  • $\ext(4) \subseteq \ext'(4)$
  • $\ext(3) \subseteq \ext'(3)$
  • $(\ent(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\} \subseteq (\ent'(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\}$
  • $(\ent(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\} \subseteq (\ent'(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\}$
  • $\ent(3) \subseteq \ent'(3)$
  • $(\ent(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\} \subseteq (\ent'(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\}$
  • $(\ent(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\} \subseteq (\ent'(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\}$
  • $(\ent(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\} \subseteq (\ent'(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\}$

I'm sure you can work it out.

$\endgroup$
1
  • $\begingroup$ This really clarifies what I need to do. And it's almost trivial. Thanks for the answer. $\endgroup$ Nov 26 '20 at 15:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.