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\\$$

然后定义$[|c|]^A=\alpha\circ[|c|]\circ\gamma$，对于某个 abstract domain $A$。那么假如$A=\textbf{Interval}$，那么：

$$\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 要做的事情

首先它们想做的事仍然是 combine proof for correctness and incorrectness，和 outcome logic 的 motivation 是一样的。

然后做法是：利用 triple 去 under-approximation 证明 incorrectness，然后利用 abstract interpretation 去 over-approximation 证明 correctness。形式化地，考虑一个 triple 和 abstract domain $A$，如果令函数$A=\gamma\circ\alpha$：

$\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$。

这三个条件其实是说，一个是$q\subseteq\text{post}[c]p\subseteq A(\text{post}[c]p)=A(q)$，即$\text{post}[c]p$ 是夹在$[q,A(q)]$ 之间的。

# Global Completeness and Local Completeness

这个定义实际上说明了：In a complete approximation $f^\#$, then only loss of precision is due to the abstract domain and not to the definition of the abstract function itself !

可以证明，$A$ is a complete abstraction for $f$ if and only if $\alpha\circ f=(\alpha\circ f\circ\gamma)\circ\alpha$ （前提是$\alpha,\gamma$ 是 Galois embedding）

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

我们记$\mathbb{C}^A(f)$ 表示 A is a complete abstraction for $f$。即$\mathbb{C}^A(f)：Af=AfA$。

其实在程序语言中，我们也希望对于所有程序$c$ 都有$\mathbb{C}^A(f)$。但这是非常罕见的情况：

…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.

所以试图引入 local completeness：

而 local 和 complete 联系就是：$\mathbb{C}^A(f)\iff\forall c\in C.\;\mathbb{C}_c^A(f)$.

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

证明：考虑到$\alpha,\gamma$ 是 Galois embedding，那么有：

$$\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<x?|]$ 和 Intervals，它不是 global complete 的，譬如对$c=\{0,4\}$ 那么：

$$A\circ[|0<x?|](c)=A(\{4\})=\{4\}\\ A\circ[|0<x?|]\circ A(c)=A\circ[|0<x?|](\{0,1,2,3,4\})=A(\{1,2,3,4\})=\{1,2,3,4\}$$

因此$A\circ[|0<x?|]\neq A\circ[|0<x?|]\circ A$。但是当$c$ 满足以下情况之一时，它是 complete 的：

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

譬如$c=\{0,1,4\}$，那么：

$$A\circ[|0<x?|](c)=A(\{1,4\})=\{1,2,3,4\}\\ A\circ[|0<x?|]\circ A(c)=A\circ[|0<x?|](\{0,1,2,3,4\})=A(\{1,2,3,4\})=\{1,2,3,4\}$$

证明：

• (=>) 假设$\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$ 证毕。