ROBERTO BRUNI, University of Pisa, Italy

ROBERTO GIACOBAZZI, University of Verona, Italy

ROBERTA GORI, University of Pisa, Italy

FRANCESCO RANZATO, University of Padova, Italy

# # 一个例子

$c_1=\textbf{if }\text{even}(x)\textbf{ then }0\textbf{ else }1\\ c_2=\textbf{if }\text{even}(x)\textbf{ then }x\textbf{ else }x+1\\$

\begin{aligned} \;[|c_1|]^{A}\circ[|c_2|]^A([0,1])&=[|c_1|]^A([0,2])\\ &=[0,1] \end{aligned}

$([|c_1|]\circ[|c_2|])^A([0,1])=[0,0]$。故有：

$([|c_1|]\circ[|c_2|])^A\subsetneq[|c_1|]^A\circ[|c_2|]^A$

The lack of compositionality is the main cause of the interdependence between the precision of an abstract interpretation and the way programs are written.

# # Correctness/Incorrectness Logic 要做的事情

$\vDash_A[p]c[q]$ 当且仅当同时满足：

1. $q\subseteq\text{post}[c]p$，即 under-approximation。
2. $A(q)=A(\text{post}[c]p)$。即有相同的 abstraction。
3. $\text{post}[c]$ is locally complete for input $p$ on $A$

# # Global Completeness and Local Completeness

Definition. The abstract domain $A$ is called a complete abstraction for $f$ if there exists a complete approximation $f^\#:A\rightarrow A$ satisfying:

$\alpha\circ f=f^\#\circ\alpha$

$A=\gamma\circ\alpha$，由于$\gamma$ 是单射，那么上述条件其实也可以等价于$A\circ f=A\circ f\circ A$

…the standard notion of (global) completeness for Boolean guards is a too strong requirement for abstract domains, often met in practice just by trivial guards or domains.

Definition. An abstract domain $A$ is locally complete for $f:C\rightarrow C$ at a concrete value $c\in C$, written $\mathbb{C}^A_c(f)$, if:

$\mathbb{C}^A_c(f)\iff Af(c)=AfA(c)$

Proposition: $\mathbb{C}_{A(c)}^A(f)$ 自然成立。($A$ is trivially locally complete for any $f$ on any abstract value $A(c)$)

\begin{aligned} AfA(A(c))&=Af\gamma\alpha\gamma\alpha(c)\\ &=Af\gamma(\alpha\gamma)\alpha(c)\\ &=AfA(c)\\ &=Af(A(c))\\ &\square. \end{aligned}

：考虑函数$[|0 和 Intervals，它不是 global complete 的，譬如对$c=\{0,4\}$ 那么：

$A\circ[|0

• $c\subseteq\mathbb{Z}_{>0}$.
• $c\subseteq\mathbb{Z}_{\leq 0}$.
• $\{0,1\}\subseteq c$.

$A\circ[|0

Theorem: $A$ is locally complete for both $[|b?|]$ and $[|\neg b?|]$ on $p$ if and only if:

$\mathbb{C}^A_p([|b?|])\text{ and }\mathbb{C}^A_p([|\neg b?|])\iff A(c)=c$

• (=>) 假设$\mathbb{C}^A_p([|b?|])\text{ and }\mathbb{C}^A_p([|\neg b?|])$，那么：

\begin{aligned} A(c)&=A(([|b?|]\circ A\circ[|b?|]p)\cup([|\neg b?|]\circ A\circ[|\neg b?|]p))\\ \text{[by monotonicity]}&\subseteq A((A\circ[|b?|]p)\cup (A\circ[|\neg b?|]p))\\ \text{[by following lemma]}&=A([|b?|]p\cup[|\neg b?|]p)\\ &=A(p) \end{aligned}

其中，我们要说明$A(A(q)\cup A(w))=A(q\cup w)$。由于 Galois embedding 可以得到$\alpha$ is additive，那么：

\begin{aligned} \gamma\alpha(A(q)\cup A(w))&=\gamma(\alpha A(q)\cup\alpha A(w))\\ &=\gamma((\alpha\gamma)\alpha(q)\cup(\alpha\gamma)\alpha(w))\\ \text{[Since Galois embedding]}&=\gamma(\alpha(q)\cup\alpha(w))\\ &=A(q\cup w)\\ &\square. \end{aligned}

因此，有：

$[|b?|]A(c)\subseteq[|b?|]A(p)\subseteq [|b?|]\circ A\circ[|b?|]\circ A(p)=[|b?|]A[|b?|](p)$

其中，第三个等号是因为 local completeness，第二个$\subseteq$ 是因为：

$\forall p.\;[|b?|]p\subseteq [|b?|]A[|b?|]p$

证明也很显然，不妨设$t\triangleq [|b?|]p$，那么因为 Galois embedding 有$t\subseteq A(t)$。那么对于任意$\sigma\in t$，都有$[|b|]_{exp}\sigma=\textbf{true}$$\sigma\in A(t)$。所以也就有$\sigma\in[|b?|]A(t)$，证毕。

因此，实际上有：

$[|b?|]A(c)\subseteq[|b?|]A[|b?|](p)\\ [|\neg b?|]A(c)\subseteq [|\neg b?|]A[|\neg b?|](p)$

所以：

\begin{aligned} A(c)&=[|b?|]A(c)\cup[|\neg b?|]A(c)\\ &\subseteq[|b?|]A[|b?|](p)\cup [|\neg b?|]A[|\neg b?|](p)\\ &=c \end{aligned}

$c\subseteq A(c)$ 是显然的，因为$A$ 的单调性，故$A(c)=c$

• (<=) 首先，我们有$p=[|b?|]p\cup[|\neg b?|]p\subseteq ([|b?|]A[|b?|]p)\cup([|\neg b?|]A[|\neg b?|]p)=c$.

所以有

$A(p)\subseteq A(c)=c=([|b?|]A[|b?|]p)\cup([|\neg b?|]A[|\neg b?|]p)$

所以有

$[|b?|]A(p)\subseteq[|b?|]c=[|b?|]A[|b?|]p\subseteq A[|b?|]p$

又因为$A\circ A=\gamma(\alpha\gamma)\alpha=\gamma\alpha=A$，故左右同时套上$A$

$A[|b?|]A(p)\subseteq AA[|b?|]p=A[|b?|]p$

此外，因为$A(p)\supseteq p$，故有$A[|b?|]A(p)\supseteq A[|b?|]p$，结合上式，故得到$A[|b?|]A(p)=A[|b?|]p$

同理也可以得到$A[|\neg b?|]A(p)=A[|\neg b?|]p$

$\square$ 证毕。