咸咸的海风吹起来初江一般的情愫,唤醒了新治本能的勇气。

考虑在 concrete domain 中的 while 的语义:

S[while  c  do  s]R=C[¬c](lfp  F)where  F(X)=RS[s](C[c]X)\mathbb{S}[while\;c\;do\;s]R=\mathbb{C}[\neg c](lfp\;F)\\ where\;F(X)=R\cup\mathbb{S}[s](\mathbb{C}[c]X)

其实就是在求状态集合上的算子FF 的最小不动点(lfp=least fixed point)。然后根据 tarski 不动点定理,对于递增链:

RF(R)F2(R)...R\subseteq F(R)\subseteq F^2(R)\subseteq...

lfp  Flfp\;F 就是 F 的不动点,即F(lfp  F)=lfp  FF(lfp\;F)=lfp\;F。一般求lfp  Flfp\;F 就是不断迭代 F,迭代次数就是循环执行的次数。


然后我们想在 abstract domain 中,不用迭代那么多步,就给出lfp  Flfp\;F 的一个 sound abstraction。这怎么办呢?我们其实可以定义一个新的二元算子类型\triangledown,它要求:

  • x#xy,y#xyx\sqsubseteq^\# x\triangledown y,y\sqsubseteq^\# x\triangledown y
  • 对于任意一个序列{xn},N,yN=yN+1\{x_n\},\exists N,y_N=y_{N+1}。其中yn=x0x1...xny_n=x_0\triangledown x_1\triangledown ...\triangledown x_n

这就是 widening operator 的定义。

然后在 abstract domain 中,会对 while 的 abstract 语义进行定义:

S#[while  c  do  s]R#=C#[¬c](lim  T#)where  T#(X#)=X#F#(X#);F#(X#)=defR##S#[s2](C#[c]X#)\mathbb{S}^\#[while\;c\;do\;s]R^\#=\mathbb{C}^\#[\neg c](lim\;T^\#)\\ where\;T^\#(X^\#)=X^\#\triangledown F^\#(X^\#);\\ F^\#(X^\#)=_{def}R^\#\cup^\#\mathbb{S}^\#[s_2](\mathbb{C}^\#[c]X^\#)

注意到几个问题,首先是lfp  Flfp\;F 对应成了lim  F#lim\;F^\#。其次原本求XF(X)X\mapsto F(X) 的最小不动点,现在对应成了X#X#F#(X#)X^\#\mapsto X^\#\triangledown F^\#(X^\#) 迭代的极限。我们其实可以说明,lim  T#lim\;T^\#就是lfp  Flfp\;F 的一个 sound abstraction,而且它一定存在(由 widening operator 的定义要求)。考虑如下序列:

X1#=R#X2#=X1#F#(X1#)X3#=X2#F#(X2#)X4#=X3#F#(X3#).....X_1^\#=R^\#\\ X_2^\#=X_1^\#\triangledown F^\#(X_1^\#)\\ X_3^\#=X_2^\#\triangledown F^\#(X_2^\#)\\ X_4^\#=X_3^\#\triangledown F^\#(X_3^\#)\\ .....

发现根据 widening operator 的定义,有X1##X2#...X_1^\#\sqsubseteq^\# X_2^\#\sqsubseteq...,即这是个递增链。再根据定义,它一定存在个极限:

Xlim#=Xlim#F#(Xlim#)X_{lim}^\#=X_{lim}^\#\triangledown F^\#(X_{lim}^\#)

所以再根据定义,有F#(Xlim#)#Xlim#F^\#(X_{lim}^\#)\sqsubseteq^\# X_{lim}^\#。再根据 Tarskian fixpoint approximation:

(Tarskian fixpoint approximation) 给定完全格(C,,,,,)(C,\leq,\vee,\wedge,\perp,\top) 上的一个单调函数f:CCf:C\rightarrow C,和它在偏序集(A,)(A,\sqsubseteq) 上的一个 sound abstraction (不一定单调)g:AAg:A\rightarrow A,那么就会有对于所有满足g(a)ag(a)\sqsubseteq aaa,它都是lfp  flfp\;f 的一个 sound abstraction。即lfp  fγ(a)lfp\;f\leq \gamma(a)

因为F#F^\#FF 的一个 sound abstraction(每一个符号都是 sound 的),所以有Xlim#X_{lim}^\#就是lfp  Flfp\;F 的一个 sound abstraction。

在实际选择中,我们可以任意选择满足要求的 widening operator,以 interval domain 举例,甚至可以[a,b][c,d]=[,+][a,b]\triangledown[c,d]=[-\infin,+\infin]。这样只需要迭代一次就找到了Xlim#=[,+]X_{lim}^\#=[-\infin,+\infin],它显然是lfp  Flfp\;F 的 sound abstraction(它是任何P(I)\mathcal{P}(\mathbb{I}) 中元素的 sound abstraction)。但是显然这没什么意义,所以我们一般选择:

[a,b][c,d]=[{aif  acotherwise,{bif  bd+otherwise][a,b]\triangledown[c,d]=[\begin{cases}a&if\;a\leq c\\-\infin&otherwise\end{cases},\begin{cases}b&if\;b\leq d\\+\infin&otherwise\end{cases}]

这样只需要O(V)O(|\mathbb{V}|) 次迭代我们就能找到Xlim#X_{lim}^\#


但是这是不够的。因为即使我们精心选择了 widening operator,可以得到lfp  Flfp\;F 的一个 sound abstraction,但它往往不够 precise。其实我们可以有一个提纯的过程(refine),即保持是 sound abstraction 的情况下,找到尽量小的那个。于是我们可以定义 narrowing operator:\triangle,要求它:

  • X##Y##X#Y##X#X^\#\sqcap^\# Y^\#\sqsubseteq^\# X^\#\triangle Y^\#\sqsubseteq^\# X^\#
  • 对于任意一个序列{Xn#},N,YN#=YN+1#\{X_n^\#\},\exists N,Y_N^\#=Y_{N+1}^\#。其中Yn#=X0#...Xn#Y_n^\#=X_0^\#\triangle...\triangle X_n^\#

它有什么作用呢?我们考虑一个迭代:X#X#F#(X#)X^\#\mapsto X^\#\triangle F^\#(X^\#)

  • 首先,它是保持 sound abstraction 的。假如X#X^\#lfp  Flfp\;F 的一个 sound abstraction,那么有lfp  Fγ(X#)lfp\;F\subseteq \gamma(X^\#)。根据 F 的单调性,有F(lfp  F)F(γ(X#))F(lfp\;F)\subseteq F(\gamma(X^\#))。再根据F#F^\#是 F 的一个 sound abstraction,就有:

    lfp  F=F(lfp  F)F(γ(X#))γ(F#(X#))lfp\;F=F(lfp\;F)\subseteq F(\gamma(X^\#))\subseteq\gamma(F^\#(X^\#))

    于是F#(X#)F^\#(X^\#) 就是lfp  Flfp\;F 的一个 sound abstraction。然后我们可以证明:若X#X^\#F#(X#)F^\#(X^\#) 都是lfp  Flfp\;F 的 sound abstraction,那么X#F#(X#)X^\#\triangle F^\#(X^\#) 也一定是lfp  Flfp\;F 的一个 sound abstraction。因为:

    lfp  Fγ(X#),lfp  Fγ(F#(X#))lfp  Fγ(X#)γ(F#(X#))γ(X##F#(X#))γ(X#F#(X#))\because lfp\;F\subseteq\gamma(X^\#),lfp\;F\subseteq\gamma(F^\#(X^\#))\\ \therefore lfp\;F\subseteq \gamma(X^\#)\cap\gamma(F^\#(X^\#))\subseteq \gamma(X^\#\sqcap^\#F^\#(X^\#))\subseteq \gamma(X^\#\triangle F^\#(X^\#))

  • 其次,它是单调减的,因为有X#F#(X#)#X#X^\#\triangle F^\#(X^\#)\sqsubseteq^\# X^\#

因此,我们可以不断迭代,直到不再变化。这样迭代的过程就是 refine 的过程(譬如不断缩小 interval),而且最后得到的 abstraction 一定仍然是 sound 的。

我们譬如可以选择:

[a,b][c,d]=[{cif  a=aotherwise,{dif  b=+botherwise][a,b]\triangle[c,d]=[\begin{cases}c&if\;a=-\infin\\a&otherwise\end{cases},\begin{cases}d&if\;b=+\infin\\b&otherwise\end{cases}]

就满足了上述要求。


所以总之,迭代 widening operator 是为了尽快找到lfp  Flfp\;F 的一个 sound abstraction;而找到后可以接着迭代 narrowing operator 对我们找到的 sound abstraction 进行提纯,使得最后得到的 abstraction 尽量 precise。