第4章 抽象解释 4.1节 将“程序分析对语言的语义是正确的”这个 概念公式化 举例 数据流分析：常量传播 一控制流分析：运行时变量所指称的函数 适度的推) 语言语义：程序参数和结果属于不同的论域 程序属性：描述它们的属性则也属于不同的论域 正确性关系：相应地，由两个关系R和R2组成 表示函数：相应地，由两个表示函数B和B组成
第4章 抽象解释 4.1 节 将“程序分析对语言的语义是正确的”这个 概念公式化 • 举例 – 数据流分析：常量传播 – 控制流分析：运行时变量所指称的函数 • 适度的推广 – 语言语义：程序参数和结果属于不同的论域 – 程序属性：描述它们的属性则也属于不同的论域 – 正确性关系：相应地，由两个关系R1和R2组成 – 表示函数：相应地，由两个表示函数1和2组成
第4章 抽象解释 4.2节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 加宽算子 上界算子 上界算子作用到一个序列，得到一个上升序列 加宽算子 1、对上升序列加宽得到的序列能够稳定 2、对单调函数f的迭代序列(f(L)n,用加宽算 子加宽后得到的序列会稳定，并且 Lp(f)
第4章 抽象解释 4.2 节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 • 加宽算子 – 上界算子 上界算子作用到一个序列，得到一个上升序列 – 加宽算子 1、对上升序列加宽得到的序列能够稳定 2、对单调函数f 的迭代序列(f n (⊥))n，用加宽算 子加宽后得到的序列会稳定，并且 lfp(f )