南京大学 《软件分析》05 Data Flow Analysis – Foundations I

前言

抽象,晦涩,难懂

另一个视角下的迭代算法

回忆数据流分析里面的迭代算法

初始化为空,用bottom(⊥)表示。

i和i+1的元组是一样的,所以结束。

此时Xi就是一个F的不动点(Fixed point)

思考

迭代算法对数据流分析生成一个算法

  • 算法保证一定能停止或者达到不动点吗说总有一个解吗li>
  • 假设可以停止,那只有一个解或者一个不动点吗有超过一个,那我们的解答是最优的吗li>
  • 什么时候算法可以达到不动点li>

为了解答这些问题,我们得开始学数学。

偏序

定义

设R是集合A上的一个二元关系,若R满足:
Ⅰ 自反性:对任意x∈A,有xRx;
Ⅱ 反对称性(即反对称关系):对任意x,y∈A,若xRy,且yRx,则x=y;
Ⅲ 传递性:对任意x, y,z∈A,若xRy,且yRz,则xRz。 [1]
则称R为A上的偏序关系,通常记作?。注意这里的?不必是指一般意义上的“小于或等于”。
若然有x?y,我们也说x排在y前面(x precedes y)

上下界

定义

考虑一个偏序集 (P, ?),集合S ? P,如果对任何一个S中的x,x ? u,u ∈ P是P的上界。
反过来,如果对任何一个S中的x,l ? x,l ∈ P是P的下界。

  • ?S能被写作 a ? b(a join b)
  • ?S能被写作 a ? b(a meet b)

一些性质

  • 不是每个偏序集都有最小上界和最大下界

回忆我们之前的问题

迭代算法对数据流分析生成一个算法

  • 算法保证一定能停止或者达到不动点吗说总有一个解吗忆输出永远不缩水,和单调性有关)
  • 假设可以停止,那只有一个解或者一个不动点吗有超过一个,那我们的解答是最优的吗li>
  • 什么时候算法可以达到不动点li>

单调性

如果对于?x, y ∈ L,x ? y ? f(x) ? f(y),函数f:L->L(L是一个格)是单调的。

不动点定理

对于全格 (L, ?),如果1)f: L->L是单调的 2)L是有限的,则f的最小不动点可以通过迭代f(⊥), f(f(⊥)), …, fk(⊥) ,最大不动点可以通过迭代f(T), f(f(T)), …, fk(T) 来获得。

证明不动点存在

声明:本站部分文章及图片源自用户投稿,如本站任何资料有侵权请您尽早请联系jinwei@zod.com.cn进行处理,非常感谢!

上一篇 2021年7月7日
下一篇 2021年7月7日

相关推荐