1
$\begingroup$

I need to prove that the binary operator $-_\pm: \mathbb{P}^\pm\times\mathbb{P}^\pm\rightarrow\mathbb{P}^\pm$ is increasing in each of its arguments, where

$$ \mathbb{P}^\pm = \{\top_\pm, \leq0,\neq0, \geq0,<0,=0,>0,\bot_\pm\} $$

are the abstract properties it operates on. They represent the "signs" of values in $\mathbb Z$.

Their concretizations are, resp.,

$$ \mathcal{P}^\pm = \{ \mathbb Z, \{z \in \mathbb Z \mid z \leq0\}, \{z \in \mathbb Z \mid z \neq0\}, \{z \in \mathbb Z \mid z \geq0\}, \ldots, \emptyset \} $$

The concretization of a sign property $s$ is given by $\gamma(s)$, where $\gamma$ is an isomorphism between the posets $(\mathcal{P}^\pm, \subseteq)$ and $(\mathbb{P}^\pm, \sqsubseteq)$, and

$$ \forall s_1,s_2\in\mathbb{P}^\pm . s_1 \sqsubseteq s_2 \iff \gamma(s_1)\subseteq\gamma(s_2). $$

I couldn't find any smart way to prove the monotonicity of $-_\pm$, so I just built an $8\times8$ "subtraction table" with $s_1-_\pm s_2$ for every possible pair of signs. For each valid $i$, let $r_i$ be the $i$-th row, and $s_i$ the property associated with $r_i$. I simply verified that if $s_i \sqsubseteq s_j$ then, for all valid $k$, $r_{ik}\sqsubseteq r_{jk}$. I did the same for the columns.

This is quite bruteforc-y, although it didn't take long thanks to the table. I'd just like to know whether this is the correct way to solve this exercise or not.

$\endgroup$
1
  • $\begingroup$ Abstract Interpretation is a formal method for statically analyzing the behavior of programs. My question is about an exercise from the book "Principles of Abstract Interpretation". $\endgroup$
    – Kiuhnm
    Oct 5, 2023 at 21:40

1 Answer 1

3
$\begingroup$

If $P$ is a property, let $\alpha(P)$ be its best sound abstraction. "Sound" means that $P\subseteq \gamma(\alpha(P))$, that is, $\alpha(P)$ overapproximates $P$. "Best" means that if $p$ is another sound abstraction of $P$, then $\alpha(P)\sqsubseteq p$, that is, $\gamma(\alpha(P))\subseteq \gamma(p)$, that is, $\alpha(P)$ is more precise.

The operator $-_\pm$ was naturally defined such that it's optimal w.r.t. the abstract properties, that is

$$ s_1 -_\pm s_2 = \alpha_\pm (\{x-y \mid x\in \gamma_\pm(s_1) \wedge y\in \gamma_\pm(s_2)\}) $$

For instance:

\begin{align} (>0) -_\pm (<0) &= \alpha_\pm(\{x \mid x>0\} -^* \{y \mid y<0\}) \\ &= \alpha_\pm(\{x \mid x>0\} +^* \{y \mid y>0\}) \\ &= \alpha_\pm(\{x \mid x>0\}) \\ &= (>0) \end{align}

where I introduced the two star operators for convenience. (I leave the trivial definition to the reader.)

Let's define $f$ as follows:

$$ f(s, t) = \{x-y \mid x\in \gamma_\pm(s) \wedge y\in \gamma_\pm(t)\} $$

Note that $s_1\ -_\pm s_2 = \alpha_\pm(f(s_1, s_2))$.

It's now easy to see that, for all valid $s_2$:

\begin{align} s_1 \sqsubseteq s_1' &\implies \gamma_\pm(s_1) \subseteq \gamma_\pm (s_1') \\ &\implies f(s_1, s_2) \subseteq f(s_1', s_2) \\ &\implies s_1 -_\pm s_2 \sqsubseteq s_1' -_\pm s_2 \end{align}

The last implication follows from the fact that $\alpha$ is also increasing. Indeed, for every properties $P$ and $Q$ such that $P \subseteq Q$, we must have $P \subseteq Q \subseteq \gamma(\alpha(Q))$, which means that $\alpha(Q)$ is also a sound abstraction for $P$. For the optimality of $\alpha$, we must thus have $\alpha(P) \sqsubseteq \alpha(Q)$, which proves the monotonicity.

We can reason analogously for $s_2$, which concludes the proof.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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